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. --- interp/notation.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index 7761606f11..47cf4ec6ef 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1807,10 +1807,10 @@ let browse_notation strict ntn map = map [] in List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l -let global_reference_of_notation test (ntn,(sc,c,_)) = +let global_reference_of_notation ~head test (ntn,(sc,c,_)) = match c with | NRef ref when test ref -> Some (ntn,sc,ref) - | NApp (NRef ref, l) when List.for_all isNVar_or_NHole l && test ref -> + | NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref -> Some (ntn,sc,ref) | _ -> None @@ -1822,14 +1822,14 @@ let error_notation_not_reference ?loc ntn = (str "Unable to interpret " ++ quote (str ntn) ++ str " as a reference.") -let interp_notation_as_global_reference ?loc test ntn sc = +let interp_notation_as_global_reference ?loc ~head test ntn sc = let scopes = match sc with | Some sc -> let scope = find_scope (find_delimiters_scope sc) in String.Map.add sc scope String.Map.empty | None -> !scope_map in let ntns = browse_notation true ntn scopes in - let refs = List.map (global_reference_of_notation test) ntns in + let refs = List.map (global_reference_of_notation ~head test) ntns in match Option.List.flatten refs with | [_,_,ref] -> ref | [] -> error_notation_not_reference ?loc ntn -- cgit v1.2.3