Merge PR #12099: More parsing/printing notation/abbreviation consistency for mixed terms and pattern

Reviewed-by: ejgallego

1 files changed, 10 insertions, 4 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 24b5dfce29..2e3fa0aa0e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -941,7 +941,7 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
   try
     (* If already bound to a term, unify the binder and the term *)
     match DAst.get (Id.List.assoc var terms) with
-    | GVar id' ->
+    | GVar id' | GRef (GlobRef.VarRef id',None) ->
        (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
        sigma
     | t ->
@@ -1147,16 +1147,22 @@ let does_not_come_from_already_eta_expanded_var glob =
   (* checked). *)
   match DAst.get glob with GVar _ -> false | _ -> true
 
+let is_var_term = function
+  (* The kind of expressions allowed to be both a term and a binding variable *)
+  | GVar _ -> true
+  | GRef (GlobRef.VarRef _,None) -> true
+  | _ -> false
+
 let rec match_ inner u alp metas sigma a1 a2 =
   let open CAst in
   let loc = a1.loc in
   match DAst.get a1, a2 with
   (* Matching notation variable *)
   | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1
-  | GVar _, NVar id2 when is_onlybinding_pattern_like_meta true id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+  | r1, NVar id2 when is_var_term r1 && is_onlybinding_pattern_like_meta true id2 metas -> bind_binding_as_term_env alp sigma id2 a1
   | r1, NVar id2 when is_onlybinding_pattern_like_meta false id2 metas -> bind_binding_as_term_env alp sigma id2 a1
-  | GVar _, NVar id2 when is_onlybinding_strict_meta id2 metas -> raise No_match
-  | GVar _, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+  | r1, NVar id2 when is_var_term r1 && is_onlybinding_strict_meta id2 metas -> raise No_match
+  | r1, NVar id2 when is_var_term r1 && is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1
   | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1
 
   (* Matching recursive notations for terms *)