Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notations.

Reviewed-by: jfehrle
Reviewed-by: gares
Reviewed-by: Zimmi48
Reviewed-by: maximedenes

4 files changed, 18 insertions, 7 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8bd77abc4a..0645636255 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -976,6 +976,9 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
    into a substitution for interpretation and based on binding/constr
    distinction *)
 
+let cases_pattern_of_id {loc;v=id} =
+  CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
+
 let cases_pattern_of_name {loc;v=na} =
   let atom = match na with Name id -> Some (qualid_of_ident ?loc id) | Anonymous -> None in
   CAst.make ?loc (CPatAtom atom)
@@ -991,16 +994,20 @@ let split_by_type ids subst =
     | NtnTypeConstr ->
        let terms,terms' = bind id scl terms terms' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
-    | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) ->
+    | NtnTypeBinder NtnBinderParsedAsConstr (AsNameOrPattern | AsStrictPattern) ->
        let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
        let binders' = Id.Map.add id ((coerce_to_cases_pattern_expr a,Explicit),(false,scl)) binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
     | NtnTypeBinder NtnBinderParsedAsConstr AsIdent ->
        let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
+       let binders' = Id.Map.add id ((cases_pattern_of_id (coerce_to_id a),Explicit),(true,scl)) binders' in
+       (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
+    | NtnTypeBinder NtnBinderParsedAsConstr AsName ->
+       let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
        let binders' = Id.Map.add id ((cases_pattern_of_name (coerce_to_name a),Explicit),(true,scl)) binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
-    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder as x) ->
-       let onlyident = (x = NtnParsedAsIdent) in
+    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnParsedAsBinder as x) ->
+       let onlyident = (x = NtnParsedAsIdent || x = NtnParsedAsName) in
        let binders,binders' = bind id (onlyident,scl) binders binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
     | NtnTypeConstrList ->
diff --git a/interp/notation.ml b/interp/notation.ml
index b5951a9c59..c35ba44aa5 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -62,10 +62,11 @@ let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
 
 let notation_binder_source_eq s1 s2 = match s1, s2 with
 | NtnParsedAsIdent,  NtnParsedAsIdent -> true
+| NtnParsedAsName,  NtnParsedAsName -> true
 | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
 | NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2
 | NtnParsedAsBinder,  NtnParsedAsBinder -> true
-| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false
+| (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false
 
 let ntpe_eq t1 t2 = match t1, t2 with
 | NtnTypeConstr, NtnTypeConstr -> true
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index f51d3bfdfb..036970ce37 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -881,7 +881,7 @@ let is_onlybinding_meta id metas =
 let is_onlybinding_pattern_like_meta isvar id metas =
   try match Id.List.assoc id metas with
       | _,NtnTypeBinder (NtnBinderParsedAsConstr
-                           (AsIdentOrPattern | AsStrictPattern)) -> true
+                           (AsNameOrPattern | AsStrictPattern)) -> true
       | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
       | _,NtnTypeBinder NtnParsedAsBinder -> not isvar
       | _ -> false
@@ -1533,7 +1533,7 @@ let match_notation_constr ~print_univ c ~vars (metas,pat) =
           let v = glob_constr_of_cases_pattern (Global.env()) pat in
           (((vars,v),scl)::terms',termlists',binders',binderlists')
         | _ -> raise No_match)
-    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder) ->
+    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnParsedAsBinder) ->
        (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists')
     | NtnTypeConstrList ->
        (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists')
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 29db23cc54..c541a19bfd 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -67,7 +67,8 @@ type extended_subscopes = Constrexpr.notation_entry_level * subscopes
 
 type constr_as_binder_kind =
   | AsIdent
-  | AsIdentOrPattern
+  | AsName
+  | AsNameOrPattern
   | AsStrictPattern
 
 type notation_binder_source =
@@ -76,6 +77,8 @@ type notation_binder_source =
   | NtnParsedAsPattern of bool
   (* This accepts only ident *)
   | NtnParsedAsIdent
+  (* This accepts only name *)
+  | NtnParsedAsName
   (* This accepts ident, or pattern, or both *)
   | NtnBinderParsedAsConstr of constr_as_binder_kind
   (* This accepts ident, _, and quoted pattern *)