diff options
| author | Maxime Dénès | 2018-03-10 10:04:56 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-10 10:04:56 +0100 |
| commit | 4d5c7243b4aea5b28358757e2d86c11334da6699 (patch) | |
| tree | ade1ab73a9c2066302145bb3781a39b5d46b4513 /tactics/hints.ml | |
| parent | 93a1c4786c9b17efdda025f754ad97376d61a9ba (diff) | |
| parent | b1d749e59444f86e40f897c41739168bb1b1b9b3 (diff) | |
Merge PR #6837: [located] Push inner locations in reference to a CAst.t node.
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index f3e0619a2d..a285d6b93f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1279,7 +1279,7 @@ let interp_hints poly = prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in let fref r = let gr = global_with_alias r in - Dumpglob.add_glob ?loc:(loc_of_reference r) gr; + Dumpglob.add_glob ?loc:r.CAst.loc gr; gr in let fr r = evaluable_of_global_reference env (fref r) in let fi c = @@ -1306,7 +1306,7 @@ let interp_hints poly = let constr_hints_of_ind qid = let ind = global_inductive_with_alias qid in let mib,_ = Global.lookup_inductive ind in - Dumpglob.dump_reference ?loc:(fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind"; + Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_reference qid) "ind"; List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in |