From 52b93b587b9cb53b0ed11c7d6cf5f328d7ee1479 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 23 Oct 2020 22:58:30 +0200
Subject: Add preliminary support for notations with large class
 (non-recursive) binders.

We introduce a class of open binders which includes "x", "x:t", "'pat"
and a class of closed binders which includes "x", "(x:t)", "'pat".
---
 interp/notation_term.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'interp/notation_term.ml')

diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 82238b71b7..47b9deccce 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -78,6 +78,8 @@ type notation_binder_source =
   | NtnParsedAsIdent
   (* This accepts ident, or pattern, or both *)
   | NtnBinderParsedAsConstr of constr_as_binder_kind
+  (* This accepts ident, _, and quoted pattern *)
+  | NtnParsedAsBinder
 
 type notation_var_instance_type =
   | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
-- 
cgit v1.2.3


From 93654a0ba50f26f90f84e98b33ec13caa92d1799 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Oct 2020 14:45:57 +0200
Subject: Enforcing when a binding variable has no explicit type in
 constr_notation.

This avoids relying on fragile invariants.
---
 interp/notation_term.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/notation_term.ml')

diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 47b9deccce..29db23cc54 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -27,8 +27,8 @@ type notation_constr =
   | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
   | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
   (* Part only in [glob_constr] *)
-  | NLambda of Name.t * notation_constr * notation_constr
-  | NProd of Name.t * notation_constr * notation_constr
+  | NLambda of Name.t * notation_constr option * notation_constr
+  | NProd of Name.t * notation_constr option * notation_constr
   | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
   | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr
   | NCases of Constr.case_style * notation_constr option *
-- 
cgit v1.2.3