diff options
Diffstat (limited to 'interp/dumpglob.ml')
| -rw-r--r-- | interp/dumpglob.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 561b0078aa..d7962e29a6 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -68,11 +68,12 @@ 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 -> (match def with - | Definition -> "def" + | Definition | Let -> "def" | Coercion -> "coe" | SubClass -> "subclass" | CanonicalStructure -> "canonstruc" @@ -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" @@ -231,7 +230,7 @@ let add_glob ?loc ref = add_glob_gen ?loc sp lib_dp ty let mp_of_kn kn = - let mp,sec,l = Names.repr_kn kn in + let mp,sec,l = Names.KerName.repr kn in Names.MPdot (mp,l) let add_glob_kn ?loc kn = |