1 files changed, 16 insertions, 14 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 4fd84eac5..a3d257154 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -231,6 +231,7 @@ type (_, _) entry =
 | TTBigint : ('self, Constrexpr.raw_natural_number) entry
 | TTConstr : prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
+| TTPattern : int -> ('self, cases_pattern_expr) entry
 | TTOpenBinderList : ('self, local_binder_expr list) entry
 | TTClosedBinderList : Tok.t list -> ('self, local_binder_expr list list) entry
 
@@ -288,6 +289,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun as
   Alist1 (symbol_of_target typ' assoc from forpat)
 | TTConstrList (typ', tkl, forpat) ->
   Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl)
+| TTPattern p -> Aentryl (Constr.pattern, p)
 | TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
 | TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
 | TTName -> Aentry Prim.name
@@ -300,16 +302,12 @@ let interp_entry forpat e = match e with
 | ETProdReference -> TTAny TTReference
 | ETProdBigint -> TTAny TTBigint
 | ETProdConstr p -> TTAny (TTConstr (p, forpat))
-| ETProdPattern -> assert false (** not used *)
+| ETProdPattern p -> TTAny (TTPattern p)
 | ETProdOther _ -> assert false (** not used *)
 | ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
 | ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
 | ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
 
-let constr_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
-  | Anonymous -> CHole (None,Misctypes.IntroAnonymous,None)
-  | Name id   -> CRef (Ident (Loc.tag ?loc id), None)
-
 let cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
   | Anonymous -> CPatAtom None
   | Name id   -> CPatAtom (Some (Ident (Loc.tag ?loc id)))
@@ -317,7 +315,8 @@ let cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
 type 'r env = {
   constrs : 'r list;
   constrlists : 'r list list;
-  binderlists : (local_binder_expr list * bool) list;
+  binders : cases_pattern_expr list;
+  binderlists : local_binder_expr list list;
 }
 
 let push_constr subst v = { subst with constrs = v :: subst.constrs }
@@ -327,11 +326,16 @@ match e with
 | TTConstr _ -> push_constr subst v
 | TTName ->
   begin match forpat with
-  | ForConstr -> push_constr subst (constr_expr_of_name v)
+  | ForConstr -> { subst with binders = cases_pattern_expr_of_name v :: subst.binders }
   | ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
   end
-| TTOpenBinderList -> { subst with binderlists = (v, true) :: subst.binderlists }
-| TTClosedBinderList _ -> { subst with binderlists = (List.flatten v, false) :: subst.binderlists }
+| TTPattern _ ->
+  begin match forpat with
+  | ForConstr -> { subst with binders = v :: subst.binders }
+  | ForPattern -> push_constr subst v
+  end
+| TTOpenBinderList -> { subst with binderlists = v :: subst.binderlists }
+| TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists }
 | TTBigint ->
   begin match forpat with
   | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral (v,true)))
@@ -431,11 +435,9 @@ let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list =
 
 let make_act : type r. r target -> _ -> r gen_eval = function
 | ForConstr -> fun notation loc env ->
-  let env = (env.constrs, env.constrlists, List.map fst env.binderlists) in
-  CAst.make ~loc @@ CNotation (notation , env)
+  let env = (env.constrs, env.constrlists, env.binders, env.binderlists) in
+  CAst.make ~loc @@ CNotation (notation, env)
 | ForPattern -> fun notation loc env ->
-  let invalid = List.exists (fun (_, b) -> not b) env.binderlists in
-  let () = if invalid then Constrexpr_ops.error_invalid_pattern_notation ~loc () in
   let env = (env.constrs, env.constrlists) in
   CAst.make ~loc @@ CPatNotation (notation, env, [])
 
@@ -451,7 +453,7 @@ let extend_constr state forpat ng =
     let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
     let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in
     let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in
-    let empty = { constrs = []; constrlists = []; binderlists = [] } in
+    let empty = { constrs = []; constrlists = []; binders = []; binderlists = [] } in
     let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
     let rule = (name, p4assoc, [Rule (symbs, act)]) in
     let r = ExtendRule (entry, reinit, (pos, [rule])) in