diff options
Diffstat (limited to 'interp/dumpglob.ml')
| -rw-r--r-- | interp/dumpglob.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 561b0078aa..e439db2b29 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 = @@ -250,12 +249,12 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc -> dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el secpath id) ) loc -let dump_definition (loc, id) sec s = +let dump_definition {CAst.loc;v=id} sec s = dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id) -let dump_constraint (((loc, n),_), _, _) sec ty = +let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty = match n with - | Names.Name id -> dump_definition (loc, id) sec ty + | Names.Name id -> dump_definition CAst.(make ?loc id) sec ty | Names.Anonymous -> () let dump_moddef ?loc mp ty = |