Fix build issue with Coq v8.9

Fixes uwplse#4
tchajed · Oct 16, 2018 · 7e24f0a · 7e24f0a
1 parent 41ff988
commit 7e24f0a
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/plugin/src/ast_plugin.ml4 b/plugin/src/ast_plugin.ml4
@@ -247,7 +247,7 @@ 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"
  | Type u -> build "Type" [build_universe u]
@@ -436,7 +436,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
 
 (*