1.0.2 version compatible with coq-8.10.2

README.md

@@ -56,7 +56,7 @@ The easiest way to install is via OPAM:
 If you want to compile it from source, you need to install the
 following dependencies:
 
-* [Coq 8.9.1](https://coq.inria.fr/) 
+* [Coq](https://coq.inria.fr/) 
 * [MetaCoq](https://github.com/MetaCoq/metacoq) 
 
 ## Usage ##

coq-switch.opam

@@ -12,12 +12,12 @@ install: [
   [make "install"]
 ]
 depends: [
-  "coq" {>= "8.9.1"}
-  "coq-metacoq-template" {>= "1.0~alpha+8.9"}
+  "coq" {>= "8.10.2"}
+  "coq-metacoq-template" {>= "1.0~alpha2+8.10"}
 ]
 tags: [
   "category:Miscellaneous/Coq Extensions"
-  "date:2019-10-09"
+  "date:2020-03-13"
   "logpath:Switch"
 ]
 synopsis: "A plugin to implement functionality similar to `switch` statement in C language."
@@ -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.1.tar.gz"
-  checksum: "51dc09401a650b0a17c8fa39780fcdb7"
+  src: "https://github.com/vzaliva/coq-switch/archive/v1.0.2.tar.gz"
+  checksum: ""
 }
 

demo.v

@@ -30,21 +30,21 @@ Section NatExample.
     | None => 0
     end.
 
-  End NatExample.
+End NatExample.
+
+Definition string_beq a b :=
+  if string_dec a b then true else false.
 
 Section StringExample.
 
   (* This example custom -> notation for choices *)
   Infix "->" := pair.
 
-  Definition string_beq a b :=
-    if string_dec a b then true else false.
-
   Run TemplateProgram
       (mkSwitch string string_beq [
                   "love" -> "SLove" ;
-                   "ten" -> "STen"  ;
-                   "twenty" -> "STwenty"
+                "ten" -> "STen"  ;
+                "twenty" -> "STwenty"
                 ] "Ex2_Choices" "ex2_select"
       ).
 

theories/Switch.v

@@ -57,7 +57,8 @@ Definition mkSwitch
           mind_entry_finite    := Finite ;
           mind_entry_params    := [] ;
           mind_entry_inds      := [one_i] ;
-          mind_entry_universes := Monomorphic_ctx ContextSet.empty ;
+          mind_entry_universes := Monomorphic_entry (LevelSet.empty, ConstraintSet.empty);
+          mind_entry_variance  := None;
           mind_entry_private   := None (* or (Some false)? *)
         |} in
     ind_t <- tmMkInductive ind ;;