From 3af3409a8ec23deb3e0d32f00a31363a36f6209b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 8 May 2020 16:29:30 +0200 Subject: Generalize the interpretation of syntactic notation as reference to their head. This seems to be a pattern used quite a bit in the wild, it does not hurt to be a bit more lenient to tolerate this kind of use. Interestingly the API was already offering a similar generalization in some unrelated places. We also backtrack on the change in Floats.FloatLemmas since it is an instance of this phenomenon. --- plugins/ltac/tacintern.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index ff1e8b92d1..fcedbe8e2e 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -97,7 +97,7 @@ let intern_global_reference ist qid = else if qualid_is_ident qid && find_hyp (qualid_basename qid) ist then let id = qualid_basename qid in ArgArg (qid.CAst.loc, GlobRef.VarRef id) - else match locate_global_with_alias qid with + else match locate_global_with_alias ~head:true qid with | r -> ArgArg (qid.CAst.loc, r) | exception Not_found -> if not !strict_check && qualid_is_ident qid then @@ -315,13 +315,13 @@ let intern_evaluable ist = function end | {v=ByNotation (ntn,sc);loc} -> let check = GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) in - let r = Notation.interp_notation_as_global_reference ?loc check ntn sc in + let r = Notation.interp_notation_as_global_reference ?loc ~head:true check ntn sc in evalref_of_globref ?loc r let intern_smart_global ist = function | {v=AN r} -> intern_global_reference ist r | {v=ByNotation (ntn,sc);loc} -> - ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc + ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc ~head:true GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)) let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid) -- cgit v1.2.3