coq-8.13 port

.gitignore

@@ -34,3 +34,4 @@ nra.cache
 /Makefile.coq.conf
 /theories/*.vos
 /.Makefile.coq.d
+*.vok

README.md

@@ -119,4 +119,4 @@ Definition Ex1 (n:nat) : T :=
 # Contact #
 
 * Repository: https://github.com/vzaliva/coq-switch
-* Questions: [Vadim Zaliva](mailto:vzaliva@cmu.edu)
+* Questions: [Vadim Zaliva](mailto:lord@crocodile.org)

coq-switch.opam

@@ -3,7 +3,7 @@ maintainer: "vzaliva@cmu.edu"
 homepage: "https://github.com/vzaliva/coq-switch"
 dev-repo: "git://git@github.com:vzaliva/coq-switch.git"
 bug-reports: "https://github.com/vzaliva/coq-switch/issues"
-authors: ["Vadim Zaliva <vzaliva@cmu.edu>"]
+authors: ["Vadim Zaliva <lord@crocodile.org>"]
 license: "MIT"
 build: [
   [make "-j%{jobs}%"]
@@ -12,15 +12,15 @@ install: [
   [make "install"]
 ]
 depends: [
-  "coq" {>= "8.12.0"}
-  "coq-metacoq-template" {>= "1.0~beta1+8.12"}
+  "coq" {>= "8.13.0"}
+  "coq-metacoq-template" {>= "1.0~beta2+8.13"}
 ]
 tags: [
   "category:Miscellaneous/Coq Extensions"
-  "date:2020-09-24"
+  "date:2021-01-28"
   "logpath:Switch"
 ]
-synopsis: "A plugin to implement functionality similar to `switch` statement in C language."
+synopsis: "A plugin to implement functionality similar to `switch` statement in C language"
 
 description: """It allows easier dispatch on several constant values
 of a type with decidable equality. Given a type, boolean equality
@@ -29,7 +29,7 @@ an inductive type with constructors, one for each of the choices, and
 a function mapping values to this type."""
 
 url {
-  src: "https://github.com/vzaliva/coq-switch/archive/v1.0.4.tar.gz"
+  src: "https://github.com/vzaliva/coq-switch/archive/v1.0.5.tar.gz"
   checksum: ""
 }
 

demo.v

@@ -30,6 +30,8 @@ MetaCoq Run
     | None => 0
     end.
 
+  Compute Ex1 10.
+
 End NatExample.
 
 Definition string_beq a b :=
@@ -60,4 +62,7 @@ Section StringExample.
     | None => 0
     end.
 
+  Compute Ex2 "ten".
+  Compute Ex2 "xxx".
+
 End StringExample.

theories/Switch.v

@@ -7,6 +7,8 @@ Import ListNotations.
 
 Open Scope string_scope.
 
+Definition rname (s:string) := {| binder_name := nNamed s; binder_relevance := Relevant |}.
+
 Fixpoint mkSwitchCases
          (type_name: kername)
          (A_t: term)
@@ -22,10 +24,10 @@ Fixpoint mkSwitchCases
   | [] => tApp (tConstruct opt_i 1 []) [tInd T_i []]
   | (x::xs) => tCase
                (* # of parameters *)
-               (bool_i, 0)
+               ((bool_i, 0), Relevant)
 
                (* type info *)
-               (tLambda (nNamed "b") (tInd bool_i []) (tApp (tInd opt_i []) [tInd T_i []]))
+               (tLambda (rname "b") (tInd bool_i []) (tApp (tInd opt_i []) [tInd T_i []]))
 
                (* discriminee *)
                (tApp P_t [tRel 0; x])
@@ -59,7 +61,7 @@ Definition mkSwitch
           mind_entry_inds      := [one_i] ;
           mind_entry_universes := Monomorphic_entry (LevelSet.empty, ConstraintSet.empty);
           mind_entry_template := false ;
-          mind_entry_cumulative  := false ;
+          mind_entry_variance := None ;
           mind_entry_private   := None (* or (Some false)? *)
         |} in
     mp <- tmCurrentModPath tt ;;
@@ -68,7 +70,7 @@ Definition mkSwitch
     A_t <- tmQuote A ;;
     P_t <- tmQuote P ;;
     choices_t <- monad_map (fun x => tmQuote (fst x)) choices ;;
-    let body_t := tLambda (nNamed "x") A_t (mkSwitchCases (mp, type_name) A_t P_t choices_t 0) in
+    let body_t := tLambda (rname "x") A_t (mkSwitchCases (mp, type_name) A_t P_t choices_t 0) in
     body <- tmUnquoteTyped (A -> option T) body_t ;;
     def_t <- tmDefinition def_name body ;;
     tmReturn tt.