Fixes to support Coq v8.9

Fixes uwplse#4
tchajed · Oct 16, 2018 · 6dae9a2 · 6dae9a2
1 parent 41ff988
commit 6dae9a2
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/README.md b/README.md
@@ -19,7 +19,7 @@ For example:
 
 ## Using the Plugin
 
-The plugin is built to work with Coq 8.8. It may not build for other versions of Coq, since the
+The plugin is built to work with Coq 8.9. It may not build for other versions of Coq, since the
 API sometimes changes between Coq versions.
 
 To build:

diff --git a/plugin/src/ast_plugin.ml4 b/plugin/src/ast_plugin.ml4
@@ -247,9 +247,10 @@ let build_universe_instance (i : Instance.t) =
  * Build the AST for a sort
  *)
 let build_sort (s : Sorts.t) =
-  let s_ast =
+  let s_ast = let open Sorts in
     match s with
-    | Prop _ -> if s = Sorts.prop then "Prop" else "Set"
+    | Prop -> "Prop"
+    | Set -> "Set"
     | Type u -> build "Type" [build_universe u]
   in build "Sort" [s_ast]
 
@@ -436,7 +437,7 @@ let build_cofix (funs : string list) (index : int) =
 (*
  * Get the body of a mutually inductive type
  *)
-let lookup_mutind_body (i : mutual_inductive) (env : env) =
+let lookup_mutind_body (i : MutInd.t) (env : env) =
   lookup_mind i env
 
 (*