diff --git a/plugin/src/ast_plugin.ml4 b/plugin/src/ast_plugin.ml4 index d2d93b2..72601e8 100644 --- 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 (*