diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 2 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 3 |
2 files changed, 2 insertions, 3 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 5be07e09e..d1b79ffcd 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -349,7 +349,7 @@ let dummy_one_inductive_entry mie = { let dummy_inductive_entry (_,m) = ([],{ mind_entry_params = []; mind_entry_record = None; - mind_entry_finite = Decl_kinds.BiFinite; + mind_entry_finite = Declarations.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty; mind_entry_private = None; diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 0197cf9ae..d7962e29a 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -68,6 +68,7 @@ let pause () = previous_state := !glob_output; glob_output := NoGlob let continue () = glob_output := !previous_state open Decl_kinds +open Declarations let type_of_logical_kind = function | IsDefinition def -> @@ -111,14 +112,12 @@ let type_of_global_ref gr = | Globnames.IndRef ind -> let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in if mib.Declarations.mind_record <> None then - let open Decl_kinds in begin match mib.Declarations.mind_finite with | Finite -> "indrec" | BiFinite -> "rec" | CoFinite -> "corec" end else - let open Decl_kinds in begin match mib.Declarations.mind_finite with | Finite -> "ind" | BiFinite -> "variant" |