diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-10 10:04:56 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-10 10:04:56 +0100 |
| commit | 4d5c7243b4aea5b28358757e2d86c11334da6699 (patch) | |
| tree | ade1ab73a9c2066302145bb3781a39b5d46b4513 /dev | |
| parent | 93a1c4786c9b17efdda025f754ad97376d61a9ba (diff) | |
| parent | b1d749e59444f86e40f897c41739168bb1b1b9b3 (diff) | |
Merge PR #6837: [located] Push inner locations in reference to a CAst.t node.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 2 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06837-ejgallego-located+libnames.sh | 15 | ||||
| -rw-r--r-- | dev/top_printers.ml | 8 |
3 files changed, 20 insertions, 5 deletions
diff --git a/dev/base_include b/dev/base_include index 3320a2a94..1fb80dc07 100644 --- a/dev/base_include +++ b/dev/base_include @@ -230,7 +230,7 @@ let pf_e gl s = let _ = Flags.in_debugger := false let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference - (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));; + (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));; let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqloop.drop_last_doc) diff --git a/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh b/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh new file mode 100644 index 000000000..a785290e7 --- /dev/null +++ b/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "6837" ] || [ "$CI_BRANCH" = "located+libnames" ]; then + + ltac2_CI_BRANCH=located+libnames + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=located+libnames + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + Elpi_CI_BRANCH=located+libnames + Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git + + coq_dpdgraph_CI_BRANCH=located+libnames + coq_dpdgraph_CI_GITURL=https://github.com/ejgallego/coq-dpdgraph.git + +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 74cdd788b..ba0c54407 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -547,7 +547,7 @@ let encode_path ?loc prefix mpdir suffix id = | Some (mp,dir) -> (DirPath.repr (dirpath_of_string (ModPath.to_string mp))@ DirPath.repr dir) in - Qualid (Loc.tag ?loc @@ make_qualid + CAst.make ?loc @@ Qualid (make_qualid (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id) let raw_string_of_ref ?loc _ = function @@ -567,9 +567,9 @@ let raw_string_of_ref ?loc _ = function encode_path ?loc "SECVAR" None [] id let short_string_of_ref ?loc _ = function - | VarRef id -> Ident (Loc.tag ?loc id) - | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (Constant.repr3 cst))) - | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (MutInd.repr3 kn))) + | 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))) | IndRef (kn,i) -> encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))] (Id.of_string ("_"^string_of_int i)) |