port to Coq-8.9.1

vzaliva · Oct 9, 2019 · 8fbf6d3 · 8fbf6d3
1 parent f8631f1
commit 8fbf6d3
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/README.md b/README.md
@@ -51,13 +51,13 @@ error-prone. This plugin allows to automate such tasks.
 The easiest way to install is via OPAM:
 
     opam repo add coq-released https://coq.inria.fr/opam/released
-    opam install --jobs=4 coq coq-template-coq coq-switch
+    opam install --jobs=4 coq coq-switch
 
 If you want to compile it from source, you need to install the
 following dependencies:
 
-* [Coq 8.8.1](https://coq.inria.fr/) 
-* [Template Coq](https://github.com/MetaCoq/metacoq)
+* [Coq 8.9.1](https://coq.inria.fr/) 
+* [MetaCoq](https://github.com/MetaCoq/metacoq) 
 
 ## Usage ##
 

diff --git a/demo.v b/demo.v
@@ -3,7 +3,7 @@ Require Import Switch.Switch.
 Require Import Coq.Arith.EqNat.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
-Require Import Template.All.
+Require Import MetaCoq.Template.All.
 
 Import ListNotations.
 

diff --git a/theories/Switch.v b/theories/Switch.v
@@ -1,6 +1,6 @@
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
-Require Import Template.All.
+Require Import MetaCoq.Template.All.
 
 Import MonadNotation.
 Import ListNotations.
@@ -57,7 +57,7 @@ Definition mkSwitch
           mind_entry_finite    := Finite ;
           mind_entry_params    := [] ;
           mind_entry_inds      := [one_i] ;
-          mind_entry_universes := Monomorphic_ctx ([], ConstraintSet.empty) ;
+          mind_entry_universes := Monomorphic_ctx ContextSet.empty ;
           mind_entry_private   := None (* or (Some false)? *)
         |} in
     ind_t <- tmMkInductive ind ;;