v1.0.4 for coq 8.12

vzaliva · Sep 24, 2020 · 91b6559 · 91b6559
1 parent d428298
commit 91b6559
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/coq-switch.opam b/coq-switch.opam
@@ -12,12 +12,12 @@ install: [
   [make "install"]
 ]
 depends: [
-  "coq" {>= "8.11.2"}
-  "coq-metacoq-template" {>= "1.0~beta1+8.11"}
+  "coq" {>= "8.12.0"}
+  "coq-metacoq-template" {>= "1.0~beta1+8.12"}
 ]
 tags: [
   "category:Miscellaneous/Coq Extensions"
-  "date:2020-09-22"
+  "date:2020-09-24"
   "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.3.tar.gz"
-  checksum: "d36f28009151751e89883bd288a89981"
+  src: "https://github.com/vzaliva/coq-switch/archive/v1.0.4.tar.gz"
+  checksum: ""
 }
 
diff --git a/theories/Switch.v b/theories/Switch.v
@@ -49,7 +49,6 @@ Definition mkSwitch
         {|
           mind_entry_typename := type_name ;
           mind_entry_arity := tSort Universe.type0 ;
-          mind_entry_template := false ;
           mind_entry_consnames := map snd choices ;
           mind_entry_lc := map (fun _ => tRel 0) choices;
         |} in
@@ -59,7 +58,8 @@ Definition mkSwitch
           mind_entry_params    := [] ;
           mind_entry_inds      := [one_i] ;
           mind_entry_universes := Monomorphic_entry (LevelSet.empty, ConstraintSet.empty);
-          mind_entry_variance  := None;
+          mind_entry_template := false ;
+          mind_entry_cumulative  := false ;
           mind_entry_private   := None (* or (Some false)? *)
         |} in
     mp <- tmCurrentModPath tt ;;