From cb105b62f597b2a51fad743547647e4885d6365a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 13 Apr 2020 20:01:29 +0200
Subject: Notations: Giving a consistent role to global references occurring
 patterns.

Currently, global references in patterns used also as terms were
accepted for parsing but not for printing.

We accept section variables for both parsing and printing. We reject
constant and inductive types for both parsing and printing.

Among other, this also fixes a hole in interpreting variables used
both patterns and terms: the term part was not interpreted.
---
 interp/notation_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 24b5dfce29..34e94d1597 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 ->
-- 
cgit v1.2.3


From c893dc56fa579c8d1f6ea3a1859681bb316d9979 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 15 Apr 2020 15:55:15 +0200
Subject: Accept section variables in notations with mixed terms and binders.

---
 interp/notation_ops.ml | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 34e94d1597..2e3fa0aa0e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -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 *)
-- 
cgit v1.2.3