Adding patterns in the category of binders for notations.

For instance, the following is now possible:

  Check {(x,y)|x+y=0}.

Some questions remains. Maybe, by consistency, the notation should be
"{'(x,y)|x+y=0}"...

11 files changed, 149 insertions, 66 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 9fe890e90..83add7a7c 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -545,6 +545,45 @@ let coerce_to_name = function
   | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name"
                          (str "This expression should be a name.")
 
+let mkAppPattern ?loc p lp =
+  let open CAst in
+  make ?loc @@ (match p.v with
+  | CPatAtom (Some r) -> CPatCstr (r, None, lp)
+  | CPatCstr (r, None, l2) ->
+     CErrors.user_err ?loc:p.loc ~hdr:"compound_pattern"
+                      (Pp.str "Nested applications not supported.")
+  | CPatCstr (r, l1, l2) -> CPatCstr (r, l1 , l2@lp)
+  | CPatNotation (n, s, l) -> CPatNotation (n , s, l@lp)
+  | _ -> CErrors.user_err
+           ?loc:p.loc ~hdr:"compound_pattern"
+           (Pp.str "Such pattern cannot have arguments."))
+
+let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
+  | CRef (r,None) ->
+     CPatAtom (Some r)
+  | CHole (None,Misctypes.IntroAnonymous,None) ->
+     CPatAtom None
+  | CLetIn ((loc,Name id),b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' ->
+      CPatAlias (coerce_to_cases_pattern_expr b, id)
+  | CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args ->
+     (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
+  | CAppExpl ((None,r,i),args) ->
+     CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[])
+  | CNotation (ntn,(c,cl,[])) ->
+     CPatNotation (ntn,(List.map coerce_to_cases_pattern_expr c,
+                        List.map (List.map coerce_to_cases_pattern_expr) cl),[])
+  | CPrim p ->
+     CPatPrim p
+  | CRecord l ->
+     CPatRecord (List.map (fun (r,p) -> (r,coerce_to_cases_pattern_expr p)) l)
+  | CDelimiters (s,p) ->
+     CPatDelimiters (s,coerce_to_cases_pattern_expr p)
+  | CCast (p,CastConv t) ->
+     CPatCast (coerce_to_cases_pattern_expr p,t)
+  | _ ->
+     CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr"
+                      (str "This expression should be coercible to a pattern.")) c
+
 let asymmetric_patterns = ref (false)
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr = false;
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 6e5c0f851..9a59d66f4 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -54,6 +54,9 @@ val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_e
 val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
 (** Same as [prod_constr_expr], with location *)
 
+val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr
+(** Apply a list of pattern arguments to a pattern *)
+
 (** @deprecated variant of mkCLambdaN *)
 val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
 [@@ocaml.deprecated "deprecated variant of mkCLambdaN"]
@@ -73,6 +76,8 @@ val coerce_to_id : constr_expr -> Id.t located
 val coerce_to_name : constr_expr -> Name.t located
 (** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *)
 
+val coerce_to_cases_pattern_expr : constr_expr -> cases_pattern_expr
+
 (** {6 Binder manipulation} *)
 
 val default_binder_kind : binder_kind
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5c9a12c29..000c7dab3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -451,7 +451,7 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p =
        il,cp
     | _ -> assert false
   in
-  let env = {env with ids = List.fold_right Id.Set.add il env.ids} in
+  let env = List.fold_right (fun id env -> push_name_env Id.Map.empty (Variable,[],[],[]) env (None,Name id)) il env in
   let na = alias_of_pat cp in
   let ienv = Name.fold_right Id.Set.remove na env.ids in
   let id = Namegen.next_name_away_with_default "pat" (alias_of_pat cp) ienv in
@@ -546,13 +546,21 @@ let find_fresh_name renaming (terms,termlists,binders) avoid id =
   next_ident_away_from id (fun id -> Id.Set.mem id fvs3)
 
 let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
- | Anonymous -> (renaming,env),Anonymous
+ | Anonymous -> (renaming,env), None, Anonymous
  | Name id ->
   try
-    (* Binders bound in the notation are considered first-order objects *)
-    let _,na as locna = coerce_to_name (fst (Id.Map.find id terms)) in
-    let env = push_name_env Id.Map.empty (Variable,[],[],[]) env locna in
-    (renaming,env), na
+    (* We instantiate binder name with patterns which may be parsed as terms *)
+    let pat = coerce_to_cases_pattern_expr (fst (Id.Map.find id terms)) in
+    let env,((pat,ids),id),na = intern_cases_pattern_as_binder ?loc:pat.CAst.loc Id.Map.empty env pat in
+    let pat, na = match DAst.get pat with
+    | PatVar na -> None, na
+    | _ ->
+       Some ((ids,pat),id), snd na in
+    (renaming,env), pat, na
+  with Not_found ->
+  try
+    (* Trying to associate a pattern *)
+    raise Not_found
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
@@ -560,7 +568,7 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
     let renaming' =
       if Id.equal id id' then renaming else Id.Map.add id id' renaming
     in
-    (renaming',env), Name id'
+    (renaming',env), None, Name id'
 
 type binder_action =
 | AddLetIn of Name.t Loc.located * constr_expr * constr_expr option
@@ -690,14 +698,14 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
     (* Two special cases to keep binder name synchronous with BinderType *)
     | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
         when Name.equal na na' ->
-        let subinfos,na = traverse_binder subst avoid subinfos na in
+        let subinfos,pat,na = traverse_binder subst avoid subinfos na in
         let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
-	DAst.make ?loc @@ GProd (na,Explicit,ty,aux subst' subinfos c')
+        DAst.make ?loc @@ GProd (na,Explicit,ty,Option.fold_right apply_cases_pattern pat (aux subst' subinfos c'))
     | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
         when Name.equal na na' ->
-        let subinfos,na = traverse_binder subst avoid subinfos na in
+        let subinfos,pat,na = traverse_binder subst avoid subinfos na in
         let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
-	DAst.make ?loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c')
+        DAst.make ?loc @@ GLambda (na,Explicit,ty,Option.fold_right apply_cases_pattern pat (aux subst' subinfos c'))
     | t ->
       glob_constr_of_notation_constr_with_binders ?loc
         (traverse_binder subst avoid) (aux subst') subinfos t
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 9ea52821c..3a3d4ffa8 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -103,9 +103,13 @@ let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
 
 let rec cases_pattern_fold_map ?loc g e = DAst.with_val (function
   | PatVar na ->
-      let e',na' = g e na in e', DAst.make ?loc @@ PatVar na'
+      let e',pat,na' = g e na in
+      e', (match pat with
+      | None -> DAst.make ?loc @@ PatVar na'
+      | Some ((_,pat),_) -> pat)
   | PatCstr (cstr,patl,na) ->
-      let e',na' = g e na in
+      let e',pat,na' = g e na in
+      if pat <> None then user_err (Pp.str "Unable to instantiate an \"as\" clause with a pattern.");
       let e',patl' = List.fold_left_map (cases_pattern_fold_map ?loc g) e patl in
       e', DAst.make ?loc @@ PatCstr (cstr,patl',na')
   )
@@ -136,6 +140,16 @@ let rec subst_glob_vars l gc = DAst.map (function
 
 let ldots_var = Id.of_string ".."
 
+let protect g e na =
+  let e',pat,na = g e na in
+  if pat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
+  e',na
+
+let apply_cases_pattern ?loc ((ids,pat),id) c =
+  let tm = DAst.make ?loc (GVar id) in
+  DAst.make ?loc @@
+    GCases (LetPatternStyle, None, [tm,(Anonymous,None)], [loc,(ids,[pat], c)])
+
 let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
   let lt x = DAst.make ?loc x in lt @@ match nc with
   | NVar id -> GVar id
@@ -153,39 +167,43 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
       let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in
       DAst.get (subst_glob_vars outerl it)
   | NLambda (na,ty,c) ->
-      let e',na = g e na in GLambda (na,Explicit,f e ty,f e' c)
+      let e',pat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) pat (f e' c))
   | NProd (na,ty,c) ->
-      let e',na = g e na in GProd (na,Explicit,f e ty,f e' c)
+      let e',pat,na = g e na in GProd (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) pat (f e' c))
   | NLetIn (na,b,t,c) ->
-      let e',na = g e na in GLetIn (na,f e b,Option.map (f e) t,f e' c)
+      let e',pat,na = g e na in
+      (match pat with
+       | None -> GLetIn (na,f e b,Option.map (f e) t,f e' c)
+       | Some pat -> DAst.get (apply_cases_pattern ?loc pat (f e' c)))
   | NCases (sty,rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
 	| None -> e',None
 	| Some (ind,nal) ->
 	  let e',nal' = List.fold_right (fun na (e',nal) ->
-	      let e',na' = g e' na in e',na'::nal) nal (e',[]) in
+              let e',na' = protect g e' na in
+              e',na'::nal) nal (e',[]) in
 	  e',Some (Loc.tag ?loc (ind,nal')) in
-	let e',na' = g e' na in
+        let e',na' = protect g e' na in
 	(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
-      let fold (idl,e) na = let (e,na) = g e na in ((Name.cons na idl,e),na) in
+      let fold (idl,e) na = let (e,pat,na) = g e na in ((Name.cons na idl,e),pat,na) in
       let eqnl' = List.map (fun (patl,rhs) ->
 	let ((idl,e),patl) =
 	  List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
 	Loc.tag (idl,patl,f e rhs)) eqnl in
       GCases (sty,Option.map (f e') rtntypopt,tml',eqnl')
   | NLetTuple (nal,(na,po),b,c) ->
-      let e',nal = List.fold_left_map g e nal in
-      let e'',na = g e na in
+      let e',nal = List.fold_left_map (protect g) e nal in
+      let e'',na = protect g e na in
       GLetTuple (nal,(na,Option.map (f e'') po),f e b,f e' c)
   | NIf (c,(na,po),b1,b2) ->
-      let e',na = g e na in
+      let e',na = protect g e na in
       GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2)
   | NRec (fk,idl,dll,tl,bl) ->
-      let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) ->
-	  let e,na = g e na in
+      let e,dll = Array.fold_left_map (List.fold_map (fun e (na,oc,b) ->
+          let e,na = protect g e na in
 	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
-      let e',idl = Array.fold_left_map (to_id g) e idl in
+      let e',idl = Array.fold_left_map (to_id (protect g)) e idl in
       GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
   | NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k)
   | NSort x -> GSort x
@@ -195,7 +213,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
 
 let glob_constr_of_notation_constr ?loc x =
   let rec aux () x =
-    glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),id)) aux () x
+    glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),None,id)) aux () x
   in aux () x
 
 (******************************************************************************)
@@ -867,28 +885,27 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
     (* TODO: look at the consequences for alp *)
     alp, add_env alp sigma var (DAst.make @@ GVar id)
 
-let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var id =
+let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c =
+  let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in
   try
     (* If already bound to a binder, unify the term and the binder *)
-    let v' = Id.List.assoc var binders in
-    let v'' = unify_id alp id v' in
-    if v' == v'' then sigma
+    let pat' = Id.List.assoc var binders in
+    let pat'' = unify_pat alp pat pat' in
+    if pat' == pat'' then sigma
     else
       let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
-      add_binding_env alp sigma var v''
-  with Not_found -> add_binding_env alp sigma var (Name id)
+      add_binding_env alp sigma var pat''
+  with Not_found -> add_binding_env alp sigma var pat
 
-let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var v =
+let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var pat =
   try
     (* If already bound to a binder possibly *)
     (* generating an alpha-renaming from unifying the new binder *)
-    let v' = Id.List.assoc var binders in
-    let alp, v'' = unify_name_upto alp v v' in
-    if v' == v'' then alp, sigma
-    else
-      let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
-      alp, add_binding_env alp sigma var v
-  with Not_found -> alp, add_binding_env alp sigma var v
+    let pat' = Id.List.assoc var binders in
+    let alp, pat = unify_pat_upto alp pat pat' in
+    let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
+    alp, add_binding_env alp sigma var pat
+  with Not_found -> alp, add_binding_env alp sigma var pat
 
 let bind_bindinglist_env alp (terms,termlists,binders,binderlists as sigma) var bl =
   let bl = List.rev bl in
@@ -932,7 +949,7 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
 
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (na1,Name id2) when is_onlybinding_meta id2 metas ->
-      bind_binding_env alp sigma id2 na1
+      bind_binding_env alp sigma id2 (DAst.make (PatVar na1))
   | (Name id1,Name id2) when is_term_meta id2 metas ->
       (* We let the non-binding occurrence define the rhs and hence reason up to *)
       (* alpha-conversion for the given occurrence of the name (see #4592)) *)
@@ -1063,7 +1080,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
   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 id1, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1
+  | r1, NVar id2 when 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 *)
@@ -1226,6 +1243,10 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
        when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) ->
      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in
      match_in u alp metas sigma b1 b2
+  | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(_,[cp],b1))]), Name id
+       when is_gvar p e && is_onlybinding_meta id metas && not (occur_glob_constr p b1) ->
+     let alp,sigma = bind_binding_env alp sigma id cp in
+     match_in u alp metas sigma b1 b2
   | _, _, Name id when is_bindinglist_meta id metas && (not isprod || na1 != Anonymous)->
       let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t)] in
       match_in u alp metas sigma b1 b2
@@ -1241,16 +1262,12 @@ and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) =
       (alp,sigma) patl1 patl2 in
   match_in u alp metas sigma rhs1 rhs2
 
-let term_of_binder bi = DAst.make @@ match bi with
-  | Name id -> GVar id
-  | Anonymous -> GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
-
 let match_notation_constr u c (metas,pat) =
   let terms,termlists,binders,binderlists =
     match_ false u ([],[]) metas ([],[],[],[]) c pat in
   (* Reorder canonically the substitution *)
   let find_binder x =
-    try term_of_binder (Id.List.assoc x binders)
+    try glob_constr_of_cases_pattern (Id.List.assoc x binders)
     with Not_found ->
       (* Happens for binders bound to Anonymous *)
       (* Find a better way to propagate Anonymous... *)
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 80348c78e..74be6f512 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -33,8 +33,11 @@ val notation_constr_of_glob_constr : notation_interp_env ->
 
 (** Re-interpret a notation as a [glob_constr], taking care of binders *)
 
+val apply_cases_pattern : ?loc:Loc.t ->
+  (Id.t list * cases_pattern) * Id.t -> glob_constr -> glob_constr
+
 val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t ->
-  ('a -> Name.t -> 'a * Name.t) ->
+  ('a -> Name.t -> 'a * ((Id.t list * cases_pattern) * Id.t) option * Name.t) ->
   ('a -> notation_constr -> glob_constr) ->
   'a -> notation_constr -> glob_constr
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index db68a75e0..4c55f3ec6 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -387,17 +387,7 @@ GEXTEND Gram
     | "10" LEFTA
       [ p = pattern; "as"; id = ident ->
         CAst.make ~loc:!@loc @@ CPatAlias (p, id)
-      | p = pattern; lp = LIST1 NEXT ->
-        (let open CAst in match p with
-	  | { v = CPatAtom (Some r) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, None, lp)
-	  | { v = CPatCstr (r, None, l2); loc } ->
-                 CErrors.user_err ?loc ~hdr:"compound_pattern"
-                 (Pp.str "Nested applications not supported.")
-	  | { v = CPatCstr (r, l1, l2) }  -> CAst.make ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp)
-	  | { v = CPatNotation (n, s, l) } -> CAst.make ~loc:!@loc @@ CPatNotation (n , s, l@lp)
-          | _ -> CErrors.user_err
-                 ?loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
-                 (Pp.str "Such pattern cannot have arguments."))
+      | p = pattern; lp = LIST1 NEXT -> mkAppPattern ~loc:!@loc p lp
       | "@"; r = Prim.reference; lp = LIST0 NEXT ->
         CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ]
     | "1" LEFTA
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index d74ad06b3..db18fab24 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -298,7 +298,7 @@ let interp_search_notation ?loc tag okey =
   let rec sub () = function
   | NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x)
   | c ->
-    glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), x) sub () c in
+    glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), None, x) sub () c in
   let _, npat = Patternops.pattern_of_glob_constr (sub () body) in
   Search.GlobSearchSubPattern npat
 
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index f3573360d..b3e6aa059 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -515,23 +515,34 @@ let add_patterns_for_params_remove_local_defs (ind,j) l =
       drop_local_defs typi l in
   Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l
 
+let add_alias ?loc na c =
+  match na with
+  | Anonymous -> c
+  | Name id -> GLetIn (na,DAst.make ?loc c,None,DAst.make ?loc (GVar id))
+
 (* Turn a closed cases pattern into a glob_constr *)
-let rec glob_constr_of_closed_cases_pattern_aux x = DAst.map_with_loc (fun ?loc -> function
-  | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None)
-  | PatCstr (cstr,l,Anonymous)  ->
+let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?loc -> function
+  | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (ConstructRef cstr,None))
+  | PatCstr (cstr,l,na)  ->
       let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in
       let l = add_patterns_for_params_remove_local_defs cstr l in
-      GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l)
+      add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux isclosed) l))
+  | PatVar (Name id) when not isclosed ->
+      GVar id
+  | PatVar Anonymous when not isclosed ->
+      GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Misctypes.IntroAnonymous,None)
   | _ -> raise Not_found
   ) x
 
 let glob_constr_of_closed_cases_pattern p = match DAst.get p with
   | PatCstr (cstr,l,na) ->
       let loc = p.CAst.loc in
-      na,glob_constr_of_closed_cases_pattern_aux (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
+      na,glob_constr_of_cases_pattern_aux true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
   | _ ->
       raise Not_found
 
+let glob_constr_of_cases_pattern p = glob_constr_of_cases_pattern_aux false p
+
 (**********************************************************************)
 (* Interpreting ltac variables *)
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index c894db18e..7a6d50114 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -80,10 +80,14 @@ val map_pattern : (glob_constr -> glob_constr) ->
 
     Take the current alias as parameter,
     @raise Not_found if translation is impossible *)
-val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern
+val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g
 
 val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob_constr_g
 
+(** A canonical encoding of cases pattern into constr such that
+    composed with [cases_pattern_of_glob_constr Anonymous] gives identity *)
+val glob_constr_of_cases_pattern : 'a cases_pattern_g -> 'a glob_constr_g
+
 val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list
 
 val ltac_interp_name : Ltac_pretype.ltac_var_map -> Name.t -> Name.t
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 9c711ff26..5bb77b8fd 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -193,3 +193,5 @@ pair
             (prod nat (prod nat nat))) (prod (prod nat nat) nat)
 fun x : nat => if x is n .+ 1 then n else 1
      : nat -> nat
+{{{x, y}} : nat * nat | x + y = 0}
+     : Set
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index d81cc702a..201198b3e 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -333,3 +333,7 @@ Notation "'if' t 'is' n .+ 1 'then' p 'else' q" :=
   (match t with S n => p | 0 => q end)
   (at level 200).
 Check fun x => if x is n.+1 then n else 1.
+
+(* Examples with binding patterns *)
+
+Check {(x,y)|x+y=0}.