diff options
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 bcc068d3d..52e3dd09f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1282,7 +1282,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_of_reference r) gr; + Dumpglob.add_glob ?loc:(loc_of_reference r) gr; gr in let fr r = evaluable_of_global_reference (Global.env()) (fref r) @@ -1311,7 +1311,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 (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind"; + Dumpglob.dump_reference ?loc:(fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind"; List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in |