diff options
Diffstat (limited to 'dev')
-rw-r--r-- | dev/base_include | 2 | ||||
-rw-r--r-- | dev/doc/changes.md | 8 | ||||
-rw-r--r-- | dev/top_printers.ml | 10 |
3 files changed, 14 insertions, 6 deletions
diff --git a/dev/base_include b/dev/base_include index 574bc097e..6f54ecb24 100644 --- a/dev/base_include +++ b/dev/base_include @@ -229,7 +229,7 @@ let pf_e gl s = let _ = Flags.in_debugger := false let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference - (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));; + (fun ?loc _ r -> Nametab.shortest_qualid_of_global ?loc Id.Set.empty r);; let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc)) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index bb8189efc..f3fc126f9 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,14 @@ ### ML API +Names + +- In `Libnames`, the type `reference` and its two constructors `Qualid` and + `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity, + `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be + replaced by a test using `qualid_is_ident`. Extracting the ident part of a + qualid can be done using `qualid_basename`. + Misctypes - Syntax for universe sorts and kinds has been moved from `Misctypes` diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 10a7a4158..844ad9188 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -549,8 +549,8 @@ let encode_path ?loc prefix mpdir suffix id = | Some (mp,dir) -> (DirPath.repr (dirpath_of_string (ModPath.to_string mp))@ DirPath.repr dir) in - CAst.make ?loc @@ Qualid (make_qualid - (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id) + make_qualid ?loc + (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id let raw_string_of_ref ?loc _ = function | ConstRef cst -> @@ -569,9 +569,9 @@ let raw_string_of_ref ?loc _ = function encode_path ?loc "SECVAR" None [] id let short_string_of_ref ?loc _ = function - | VarRef id -> CAst.make ?loc @@ Ident id - | ConstRef cst -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (Constant.repr3 cst))) - | IndRef (kn,0) -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (MutInd.repr3 kn))) + | VarRef id -> qualid_of_ident ?loc id + | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (pi3 (Constant.repr3 cst))) + | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (pi3 (MutInd.repr3 kn))) | IndRef (kn,i) -> encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))] (Id.of_string ("_"^string_of_int i)) |