Adding ability to put any pattern in binders, prefixed by a quote.

Cf CHANGES for details.

8 files changed, 271 insertions, 71 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index c5730e626..f49ed9a5f 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -40,7 +40,7 @@ let names_of_local_assums bl =
   List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
 
 let names_of_local_binders bl =
-  List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
+  List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalPattern _ -> assert false) bl)
 
 (**********************************************************************)
 (* Functions on constr_expr *)
@@ -260,6 +260,7 @@ let cases_pattern_expr_loc = function
   | CPatRecord (loc, _) -> loc
   | CPatPrim (loc,_) -> loc
   | CPatDelimiters (loc,_,_) -> loc
+  | CPatCast(loc,_,_) -> loc
 
 let raw_cases_pattern_expr_loc = function
   | RCPatAlias (loc,_,_) -> loc
@@ -271,6 +272,7 @@ let local_binder_loc = function
   | LocalRawAssum ((loc,_)::_,_,t)
   | LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t)
   | LocalRawAssum ([],_,_) -> assert false
+  | LocalPattern (loc,_,_) -> loc
 
 let local_binders_loc bll = match bll with
   | [] -> Loc.ghost
@@ -292,23 +294,74 @@ let mkAppC (f,l) =
   | CApp (_,g,l') -> CApp (Loc.ghost, g, l' @ l)
   | _ -> CApp (Loc.ghost, (None, f), l)
 
-let rec mkCProdN loc bll c =
-  match bll with
-  | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
-      CProdN (loc,[idl,bk,t],mkCProdN (Loc.merge loc1 loc) bll c)
-  | LocalRawDef ((loc1,_) as id,b) :: bll ->
-      CLetIn (loc,id,b,mkCProdN (Loc.merge loc1 loc) bll c)
-  | [] -> c
-  | LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c
-
-let rec mkCLambdaN loc bll c =
-  match bll with
-  | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
-      CLambdaN (loc,[idl,bk,t],mkCLambdaN (Loc.merge loc1 loc) bll c)
-  | LocalRawDef ((loc1,_) as id,b) :: bll ->
-      CLetIn (loc,id,b,mkCLambdaN (Loc.merge loc1 loc) bll c)
-  | [] -> c
-  | LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c
+let add_name_in_env env n =
+  match snd n with
+  | Anonymous -> env
+  | Name id -> id :: env
+
+let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) ()
+
+let expand_pattern_binders mkC bl c =
+  let rec loop bl c =
+    match bl with
+    | [] -> ([], [], c)
+    | b :: bl ->
+        let (env, bl, c) = loop bl c in
+        match b with
+        | LocalRawDef (n, _) ->
+            let env = add_name_in_env env n in
+            (env, b :: bl, c)
+        | LocalRawAssum (nl, _, _) ->
+            let env = List.fold_left add_name_in_env env nl in
+            (env, b :: bl, c)
+        | LocalPattern (loc, p, ty) ->
+            let ni = Hook.get fresh_var env c in
+            let id = (loc, Name ni) in
+            let b =
+              LocalRawAssum
+                ([id], Default Explicit,
+                 match ty with
+                 | Some ty -> ty
+                 | None -> CHole (loc, None, IntroAnonymous, None))
+            in
+            let e = CRef (Libnames.Ident (loc, ni), None) in
+            let c =
+              CCases
+                (loc, LetPatternStyle, None, [(e,None,None)],
+                 [(loc, [(loc,[p])], mkC loc bl c)])
+            in
+            (ni :: env, [b], c)
+  in
+  let (_, bl, c) = loop bl c in
+  (bl, c)
+
+let mkCProdN loc bll c =
+  let rec loop loc bll c =
+    match bll with
+    | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+        CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
+    | LocalRawDef ((loc1,_) as id,b) :: bll ->
+        CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
+    | [] -> c
+    | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
+    | LocalPattern (loc,p,ty) :: bll -> assert false
+  in
+  let (bll, c) = expand_pattern_binders loop bll c in
+  loop loc bll c
+
+let mkCLambdaN loc bll c =
+  let rec loop loc bll c =
+    match bll with
+    | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+        CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
+    | LocalRawDef ((loc1,_) as id,b) :: bll ->
+        CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
+    | [] -> c
+    | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
+    | LocalPattern (loc,p,ty) :: bll -> assert false
+  in
+  let (bll, c) = expand_pattern_binders loop bll c in
+  loop loc bll c
 
 let rec abstract_constr_expr c = function
   | [] -> c
@@ -316,6 +369,7 @@ let rec abstract_constr_expr c = function
   | LocalRawAssum (idl,bk,t)::bl ->
       List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
       (abstract_constr_expr c bl)
+  | LocalPattern _::_ -> assert false
 
 let rec prod_constr_expr c = function
   | [] -> c
@@ -323,6 +377,7 @@ let rec prod_constr_expr c = function
   | LocalRawAssum (idl,bk,t)::bl ->
       List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
       (prod_constr_expr c bl)
+  | LocalPattern _::_ -> assert false
 
 let coerce_reference_to_id = function
   | Ident (_,id) -> id
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 3f5be4855..a92da035f 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -58,6 +58,11 @@ val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr
 val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr
 (** Same as [prod_constr_expr], with location *)
 
+val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t
+val expand_pattern_binders :
+  (Loc.t -> local_binder list -> constr_expr -> constr_expr) ->
+  local_binder list -> constr_expr -> local_binder list * constr_expr
+
 (** {6 Destructors}*)
 
 val coerce_reference_to_id : reference -> Id.t
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 82fa85f69..99b229251 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -765,6 +765,7 @@ let rec extern inctx scopes vars r =
 	     let listdecl =
 	       Array.mapi (fun i fi ->
                  let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
+                 let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) bl in
                  let (assums,ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
                  let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
@@ -781,7 +782,8 @@ let rec extern inctx scopes vars r =
 	 | GCoFix n ->
 	     let listdecl =
                Array.mapi (fun i fi ->
-                 let (_,ids,bl) = extern_local_binder scopes vars blv.(i) in
+                 let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) blv.(i) in
+                 let (_,ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
                  let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
 		 ((Loc.ghost, fi),bl,extern_typ scopes vars0 tyv.(i),
@@ -824,13 +826,13 @@ and factorize_lambda inctx scopes vars na bk aty c =
 
 and extern_local_binder scopes vars = function
     [] -> ([],[],[])
-  | (na,bk,Some bd,ty)::l ->
+  | (Inl na,bk,Some bd,ty)::l ->
       let (assums,ids,l) =
         extern_local_binder scopes (name_fold Id.Set.add na vars) l in
       (assums,na::ids,
        LocalRawDef((Loc.ghost,na), extern false scopes vars bd) :: l)
 
-  | (na,bk,None,ty)::l ->
+  | (Inl na,bk,None,ty)::l ->
       let ty = extern_typ scopes vars ty in
       (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with
           (assums,ids,LocalRawAssum(nal,k,ty')::l)
@@ -843,6 +845,14 @@ and extern_local_binder scopes vars = function
             (na::assums,na::ids,
              LocalRawAssum([(Loc.ghost,na)],Default bk,ty) :: l))
 
+  | (Inr p,bk,Some bd,ty)::l -> assert false
+
+  | (Inr p,bk,None,ty)::l ->
+      let ty = extern_typ scopes vars ty in
+      let p = extern_cases_pattern vars p in
+      let (assums,ids,l) = extern_local_binder scopes vars l in
+      (assums,ids, LocalPattern(Loc.ghost,p,Some ty) :: l)
+
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
    extern inctx scopes vars c)
@@ -1050,4 +1060,5 @@ let extern_constr_pattern env sigma pat =
 let extern_rel_context where env sigma sign =
   let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
   let vars = vars_of_env env in
+  let a = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) a in
   pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0c02c5dab..ff1fd929b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -369,7 +369,7 @@ let check_hidden_implicit_parameters id impls =
     errorlabstrm "" (strbrk "A parameter of an inductive type " ++
     pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
 
-let push_name_env ?(global_level=false) lvar implargs env =
+let push_name_env ?(global_level=false) ntnvars implargs env =
   function
   | loc,Anonymous ->
       if global_level then
@@ -377,7 +377,6 @@ let push_name_env ?(global_level=false) lvar implargs env =
       env
   | loc,Name id ->
       check_hidden_implicit_parameters id env.impls ;
-      let (_,ntnvars) = lvar in
       if Id.Map.is_empty ntnvars && Id.equal id ldots_var
         then error_ldots_var loc;
       set_var_scope loc id false env ntnvars;
@@ -433,14 +432,72 @@ let intern_assumption intern lvar env nal bk ty =
      let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
      env, b
 
+let obj_string x =
+  if Obj.is_block (Obj.repr x) then
+    "tag = " ^ string_of_int (Obj.tag (Obj.repr x))
+  else "int_val = " ^ string_of_int (Obj.magic x)
+
+let rec free_vars_of_pat il =
+  function
+  | CPatCstr (loc, c, l1, l2) ->
+      let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in
+      List.fold_left free_vars_of_pat il l2
+  | CPatAtom (loc, ro) ->
+      begin match ro with
+      | Some (Ident (loc, i)) -> (loc, i) :: il
+      | Some _ | None -> il
+      end
+  | CPatNotation (loc, n, l1, l2) ->
+      let il = List.fold_left free_vars_of_pat il (fst l1) in
+      List.fold_left (List.fold_left free_vars_of_pat) il (snd l1)
+  | _ -> anomaly (str "free_vars_of_pat")
+
+let intern_local_pattern intern lvar env p =
+  List.fold_left
+    (fun env (loc, i) ->
+       let bk = Default Implicit in
+       let ty = CHole (loc, None, Misctypes.IntroAnonymous, None) in
+       let n = Name i in
+       let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in
+       env)
+    env (free_vars_of_pat [] p)
+
+type binder_data =
+  | BDRawDef of (Loc.t * glob_binder)
+  | BDPattern of
+      (Loc.t * (cases_pattern * Id.t list) *
+         (bool ref *
+          (Notation_term.tmp_scope_name option *
+           Notation_term.tmp_scope_name list)
+          option ref * Notation_term.notation_var_internalization_type)
+         Names.Id.Map.t *
+       intern_env * constr_expr)
+
+let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
+
 let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function
   | LocalRawAssum(nal,bk,ty) ->
       let env, bl' = intern_assumption intern lvar env nal bk ty in
+      let bl' = List.map (fun a -> BDRawDef a) bl' in
       env, bl' @ bl
   | LocalRawDef((loc,na as locna),def) ->
       let indef = intern env def in
       (push_name_env lvar (impls_term_list indef) env locna,
-      (loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)))::bl)
+       (BDRawDef ((loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)))))::bl)
+  | LocalPattern (loc,p,ty) ->
+      let tyc =
+        match ty with
+        | Some ty -> ty
+        | None -> CHole(loc,None,Misctypes.IntroAnonymous,None)
+      in
+      let env = intern_local_pattern intern lvar env p in
+      let cp =
+        match !intern_cases_pattern_fwd (None,env.scopes) p with
+        | (_, [(_, cp)]) -> cp
+        | _ -> assert false
+      in
+      let il = List.map snd (free_vars_of_pat [] p) in
+      (env, BDPattern(loc,(cp,il),lvar,env,tyc) :: bl)
 
 let intern_generalization intern env lvar loc bk ak c =
   let c = intern {env with unb = true} c in
@@ -509,16 +566,36 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
     in
     (renaming',env), Name id'
 
-let make_letins = List.fold_right (fun (loc,(na,b,t)) c -> GLetIn (loc,na,b,c))
-
-let rec subordinate_letins letins = function
+type letin_param =
+  | LPLetIn of Loc.t * (Name.t * glob_constr)
+  | LPCases of Loc.t * (cases_pattern * Id.t list) * Id.t
+
+let make_letins =
+  List.fold_right
+    (fun a c ->
+     match a with
+     | LPLetIn (loc,(na,b)) ->
+         GLetIn(loc,na,b,c)
+     | LPCases (loc,(cp,il),id) ->
+         let tt = (GVar(loc,id),(Name id,None)) in
+         GCases(loc,Misctypes.LetPatternStyle,None,[tt],[(loc,il,[cp],c)]))
+
+let rec subordinate_letins intern letins = function
   (* binders come in reverse order; the non-let are returned in reverse order together *)
   (* with the subordinated let-in in writing order *)
-  | (loc,(na,_,Some b,t))::l ->
-      subordinate_letins ((loc,(na,b,t))::letins) l
-  | (loc,(na,bk,None,t))::l ->
-      let letins',rest = subordinate_letins [] l in
+  | BDRawDef (loc,(na,_,Some b,t))::l ->
+      subordinate_letins intern (LPLetIn (loc,(na,b))::letins) l
+  | BDRawDef (loc,(na,bk,None,t))::l ->
+      let letins',rest = subordinate_letins intern [] l in
       letins',((loc,(na,bk,t)),letins)::rest
+  | BDPattern (loc,u,lvar,env,tyc) :: l ->
+      let ienv = Id.Set.elements env.ids in
+      let id = Namegen.next_ident_away (Id.of_string "pat") ienv in
+      let na = (loc, Name id) in
+      let bk = Default Explicit in
+      let _, bl' = intern_assumption intern lvar env [na] bk tyc in
+      let bl' = List.map (fun a -> BDRawDef a) bl' in
+      subordinate_letins intern (LPCases (loc,u,id)::letins) (bl'@ l)
   | [] ->
       letins,[]
 
@@ -526,7 +603,7 @@ let rec subst_iterator y t = function
   | GVar (_,id) as x -> if Id.equal id y then t else x
   | x -> map_glob_constr (subst_iterator y t) x
 
-let instantiate_notation_constr loc intern (_,ntnvars as lvar) subst infos c =
+let instantiate_notation_constr loc intern ntnvars subst infos c =
   let (terms,termlists,binders) = subst in
   (* when called while defining a notation, avoid capturing the private binders
      of the expression by variables bound by the notation (see #3892) *)
@@ -585,8 +662,8 @@ let instantiate_notation_constr loc intern (_,ntnvars as lvar) subst infos c =
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
 	let (bl,(scopt,subscopes)) = Id.Map.find x binders in
-	let env,bl = List.fold_left (intern_local_binder_aux intern lvar) (env,[]) bl in
-	let letins,bl = subordinate_letins [] bl in
+	let env,bl = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in
+	let letins,bl = subordinate_letins intern [] bl in
         let termin = aux subst' (renaming,env) terminator in
 	let res = List.fold_left (fun t binder ->
           subst_iterator ldots_var t
@@ -596,11 +673,14 @@ let instantiate_notation_constr loc intern (_,ntnvars as lvar) subst infos c =
       with Not_found ->
           anomaly (Pp.str "Inconsistent substitution of recursive notation"))
     | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt ->
-        let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in
-	GProd (loc,na,bk,t,make_letins letins (aux subst' infos c'))
+        let a,letins = snd (Option.get binderopt) in
+        let e = make_letins letins (aux subst' infos c') in
+        let (loc,(na,bk,t)) = a in
+        GProd (loc,na,bk,t,e)
     | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt ->
-        let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in
-	GLambda (loc,na,bk,t,make_letins letins (aux subst' infos c'))
+        let a,letins = snd (Option.get binderopt) in
+        let (loc,(na,bk,t)) = a in
+        GLambda (loc,na,bk,t,make_letins letins (aux 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' ->
@@ -775,10 +855,10 @@ let intern_non_secvar_qualid loc qid intern env lvar us args =
     | GRef (_, VarRef _, _),_,_ -> raise Not_found
     | r -> r
 
-let intern_applied_reference intern env namedctx lvar us args = function
+let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function
   | Qualid (loc, qid) ->
       let r,projapp,args2 =
-	try intern_qualid loc qid intern env lvar us args
+	try intern_qualid loc qid intern env ntnvars us args
 	with Not_found -> error_global_not_found_loc loc qid
       in
       let x, imp, scopes, l = find_appl_head_data r in
@@ -788,7 +868,7 @@ let intern_applied_reference intern env namedctx lvar us args = function
       with Not_found ->
       let qid = qualid_of_ident id in
       try
-	let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env lvar us args in
+	let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env ntnvars us args in
 	let x, imp, scopes, l = find_appl_head_data r in
 	  (x,imp,scopes,l), args2
       with Not_found ->
@@ -1195,6 +1275,8 @@ let drop_notations_pattern looked_for =
     | CPatAtom (loc,None) -> RCPatAtom (loc,None)
     | CPatOr (loc, pl) ->
       RCPatOr (loc,List.map (in_pat top scopes) pl)
+    | CPatCast _ ->
+      assert false
   and in_pat_sc scopes x = in_pat false (x,snd scopes)
   and in_not top loc scopes (subst,substlist as fullsubst) args = function
     | NVar id ->
@@ -1280,6 +1362,10 @@ let intern_cases_pattern genv scopes aliases pat =
   intern_pat genv aliases
     (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat)
 
+let _ =
+  intern_cases_pattern_fwd :=
+    fun scopes p -> intern_cases_pattern (Global.env ()) scopes empty_alias p
+
 let intern_ind_pattern genv scopes pat =
   let no_not =
     try
@@ -1362,7 +1448,7 @@ let extract_explicit_arg imps args =
 (**********************************************************************)
 (* Main loop                                                          *)
 
-let internalize globalenv env allow_patvar lvar c =
+let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
   let rec intern env = function
     | CRef (ref,us) as x ->
 	let (c,imp,subscopes,l),_ =
@@ -1383,10 +1469,11 @@ let internalize globalenv env allow_patvar lvar c =
           (fun (id,(n,order),bl,ty,_) ->
 	     let intern_ro_arg f =
 	       let before, after = split_at_annot bl n in
-	       let (env',rbefore) =
-		 List.fold_left intern_local_binder (env,[]) before in
+	       let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
+               let rbefore = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbefore in
 	       let ro = f (intern env') in
 	       let n' = Option.map (fun _ -> List.count (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore) n in
+               let rbefore = List.map (fun a -> BDRawDef a) rbefore in
 		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
 	     in
 	     let n, ro, (env',rbl) =
@@ -1398,12 +1485,18 @@ let internalize globalenv env allow_patvar lvar c =
 	       | CMeasureRec (m,r) ->
 		   intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r))
 	     in
-	       ((n, ro), List.rev rbl, intern_type env' ty, env')) dl in
+	     let bl =
+               List.rev_map
+                 (function
+                  | BDRawDef a -> a
+                  | BDPattern (loc,_,_,_,_) ->
+                      Loc.raise loc (Stream.Error "pattern with quote not allowed after fix")) rbl in
+	       ((n, ro), bl, intern_type env' ty, env')) dl in
         let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
 	     let env'' = List.fold_left_i (fun i en name -> 
 					     let (_,bli,tyi,_) = idl_temp.(i) in
 					     let fix_args = (List.map (fun (_,(na, bk, _, _)) -> (build_impls bk na)) bli) in
-					       push_name_env lvar (impls_type_list ~args:fix_args tyi)
+					       push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
 					    en (Loc.ghost, Name name)) 0 env' lf in
              (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
 	GRec (loc,GFix
@@ -1422,15 +1515,15 @@ let internalize globalenv env allow_patvar lvar c =
 	in
         let idl_tmp = Array.map
           (fun ((loc,id),bl,ty,_) ->
-            let (env',rbl) =
-              List.fold_left intern_local_binder (env,[]) bl in
+            let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in
+            let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbl in
             (List.rev rbl,
              intern_type env' ty,env')) dl in
 	let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') ->
 	     let env'' = List.fold_left_i (fun i en name ->
 					     let (bli,tyi,_) = idl_tmp.(i) in
 					     let cofix_args =  List.map (fun (_, (na, bk, _, _)) -> (build_impls bk na)) bli in
-	       push_name_env lvar (impls_type_list ~args:cofix_args tyi)
+	       push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
 					    en (Loc.ghost, Name name)) 0 env' lf in
              (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
 	GRec (loc,GCoFix n,
@@ -1449,15 +1542,15 @@ let internalize globalenv env allow_patvar lvar c =
     | CLetIn (loc,na,c1,c2) ->
 	let inc1 = intern (reset_tmp_scope env) c1 in
 	GLetIn (loc, snd na, inc1,
-          intern (push_name_env lvar (impls_term_list inc1) env na) c2)
+          intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
     | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[]))
 	when Bigint.is_strictly_pos p ->
 	intern env (CPrim (loc,Numeral (Bigint.neg p)))
     | CNotation (_,"( _ )",([a],[],[])) -> intern env a
     | CNotation (loc,ntn,args) ->
-        intern_notation intern env lvar loc ntn args
+        intern_notation intern env ntnvars loc ntn args
     | CGeneralization (loc,b,a,c) ->
-        intern_generalization intern env lvar loc b a c
+        intern_generalization intern env ntnvars loc b a c
     | CPrim (loc, p) ->
 	fst (Notation.interp_prim_token loc p (env.tmp_scope,env.scopes))
     | CDelimiters (loc, key, e) ->
@@ -1485,7 +1578,7 @@ let internalize globalenv env allow_patvar lvar c =
 	       intern_applied_reference intern env
 		 (Environ.named_context globalenv) lvar us args ref
             | CNotation (loc,ntn,([],[],[])) ->
-                let c = intern_notation intern env lvar loc ntn ([],[],[]) in
+                let c = intern_notation intern env ntnvars loc ntn ([],[],[]) in
                 let x, impl, scopes, l = find_appl_head_data c in
 		  (x,impl,scopes,l), args
             | x -> (intern env f,[],[],[]), args in
@@ -1518,7 +1611,7 @@ let internalize globalenv env allow_patvar lvar c =
 	    (tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs)
 	  tms ([],Id.Set.empty,[]) in
         let env' = Id.Set.fold
-	  (fun var bli -> push_name_env lvar (Variable,[],[],[]) bli (Loc.ghost,Name var))
+	  (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (Loc.ghost,Name var))
 	  (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in
         (* PatVars before a real pattern do not need to be matched *)
         let stripped_match_from_in =
@@ -1552,16 +1645,16 @@ let internalize globalenv env allow_patvar lvar c =
 	(* "in" is None so no match to add *)
         let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
         let p' = Option.map (fun u ->
-	  let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
+	  let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
 	    (Loc.ghost,na') in
 	  intern_type env'' u) po in
         GLetTuple (loc, List.map snd nal, (na', p'), b',
-                   intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
+                   intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
     | CIf (loc, c, (na,po), b1, b2) ->
       let env' = reset_tmp_scope env in
       let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
       let p' = Option.map (fun p ->
-          let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
+          let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
 	    (Loc.ghost,na') in
 	  intern_type env'' p) po in
         GIf (loc, c', (na', p'), intern env b1, intern env b2)
@@ -1606,7 +1699,7 @@ let internalize globalenv env allow_patvar lvar c =
   and intern_type env = intern (set_type_scope env)
 
   and intern_local_binder env bind =
-    intern_local_binder_aux intern lvar env bind
+    intern_local_binder_aux intern ntnvars env bind
 
   (* Expands a multiple pattern into a disjunction of multiple patterns *)
   and intern_multiple_pattern env n (loc,pl) =
@@ -1685,11 +1778,11 @@ let internalize globalenv env allow_patvar lvar c =
     (tm',(snd na,typ)), extra_id, match_td
 
   and iterate_prod loc2 env bk ty body nal =
-    let env, bl = intern_assumption intern lvar env nal bk ty in
+    let env, bl = intern_assumption intern ntnvars env nal bk ty in
     it_mkGProd loc2 bl (intern_type env body)
 
   and iterate_lam loc2 env bk ty body nal =
-    let env, bl = intern_assumption intern lvar env nal bk ty in
+    let env, bl = intern_assumption intern ntnvars env nal bk ty in
     it_mkGLambda loc2 bl (intern env body)
 
   and intern_impargs c env l subscopes args =
@@ -1895,7 +1988,16 @@ let intern_context global_level env impl_env binders =
   try
   let lvar = (empty_ltac_sign, Id.Map.empty) in
   let lenv, bl = List.fold_left
-	    (intern_local_binder_aux ~global_level (my_intern_constr env lvar) lvar)
+	    (fun (lenv, bl) b ->
+               let bl = List.map (fun a -> BDRawDef a) bl in
+	       let (env, bl) = intern_local_binder_aux ~global_level (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in
+               let bl =
+                 List.map
+                   (function
+                    | BDRawDef a -> a
+                    | BDPattern (loc,_,_,_,_) ->
+                        Loc.raise loc (Stream.Error "pattern with quote not allowed here")) bl in
+	       (env, bl))
 	    ({ids = extract_ids env; unb = false;
 	      tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
   (lenv.impls, List.map snd bl)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 567150a5d..b50732e4e 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -112,6 +112,7 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) =
 	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
 	  aux (Id.Set.union (ids_of_list bound) bdvars) l' tl
 
+    | LocalPattern _ :: tl -> assert false
     | [] -> bdvars, l
   in aux bound l binders
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 3efd50b17..d8e022ce6 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -692,12 +692,12 @@ let glue_letin_with_decls = true
 
 let rec match_iterated_binders islambda decls = function
   | GLambda (_,na,bk,t,b) when islambda ->
-      match_iterated_binders islambda ((na,bk,None,t)::decls) b
+      match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
   | GProd (_,(Name _ as na),bk,t,b) when not islambda ->
-      match_iterated_binders islambda ((na,bk,None,t)::decls) b
+      match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
   | GLetIn (loc,na,c,b) when glue_letin_with_decls ->
       match_iterated_binders islambda
-	((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b
+	((Inl na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b
   | b -> (decls,b)
 
 let remove_sigma x (terms,onlybinders,termlists,binderlists) =
@@ -756,14 +756,27 @@ let rec match_ inner u alp metas sigma a1 a2 =
   | r1, NList (x,_,iter,termin,lassoc) ->
       match_alist (match_hd u alp) metas sigma r1 x iter termin lassoc
 
+  (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
+  | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],t)])),
+    NBinderList (x,_,NLambda (Name id2,_,b2),(NVar v as termin)) when p = e ->
+      let decls = [(Inr cp,bk,None,t1)] in
+      match_in u alp metas (add_bindinglist_env sigma x decls) t termin
+
   (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
   | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name id2,_,b2),termin)->
-      let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in
+      let (decls,b) = match_iterated_binders true [(Inl na1,bk,None,t1)] b1 in
       (* TODO: address the possibility that termin is a Lambda itself *)
       match_in u alp metas (add_bindinglist_env sigma x decls) b termin
+
+  (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
+  | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],t)])),
+    NBinderList (x,_,NProd (Name id2,_,b2),(NVar v as termin)) when p = e ->
+      let decls = [(Inr cp,bk,None,t1)] in
+      match_in u alp metas (add_bindinglist_env sigma x decls) t termin
+
   | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name id2,_,b2),termin)
       when na1 != Anonymous ->
-      let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in
+      let (decls,b) = match_iterated_binders false [(Inl na1,bk,None,t1)] b1 in
       (* TODO: address the possibility that termin is a Prod itself *)
       match_in u alp metas (add_bindinglist_env sigma x decls) b termin
   (* Matching recursive notations for binders: general case *)
@@ -773,10 +786,10 @@ let rec match_ inner u alp metas sigma a1 a2 =
   (* Matching individual binders as part of a recursive pattern *)
   | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2)
       when is_bindinglist_meta id metas ->
-      match_in u alp metas (add_bindinglist_env sigma id [(na,bk,None,t)]) b1 b2
+      match_in u alp metas (add_bindinglist_env sigma id [(Inl na,bk,None,t)]) b1 b2
   | GProd (_,na,bk,t,b1), NProd (Name id,_,b2)
       when is_bindinglist_meta id metas && na != Anonymous ->
-      match_in u alp metas (add_bindinglist_env sigma id [(na,bk,None,t)]) b1 b2
+      match_in u alp metas (add_bindinglist_env sigma id [(Inl na,bk,None,t)]) b1 b2
 
   (* Matching compositionally *)
   | GVar (_,id1), NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
@@ -863,7 +876,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
       | _ -> assert false in
       let (alp,sigma) =
         if is_bindinglist_meta id metas then
-          alp, add_bindinglist_env sigma id [(Name id',Explicit,None,t1)]
+          alp, add_bindinglist_env sigma id [(Inl (Name id'),Explicit,None,t1)]
         else
           match_names metas (alp,sigma) (Name id') na in
       match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2
@@ -891,6 +904,10 @@ let term_of_binder = function
   | Name id -> GVar (Loc.ghost,id)
   | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
 
+type glob_decl2 =
+    (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
+      glob_constr option * glob_constr
+
 let match_notation_constr u c (metas,pat) =
   let terms,binders,termlists,binderlists =
     match_ false u ([],[]) metas ([],[],[],[]) c pat in
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 576c5b943..0f1b1a875 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -47,9 +47,12 @@ val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr
 
 exception No_match
 
+type glob_decl2 =
+    (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
+      glob_constr option * glob_constr
 val match_notation_constr : bool -> glob_constr -> interpretation ->
       (glob_constr * subscopes) list * (glob_constr list * subscopes) list *
-      (glob_decl list * subscopes) list
+      (glob_decl2 list * subscopes) list
 
 val match_notation_constr_cases_pattern :
   cases_pattern -> interpretation ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 91099bbb1..4109bdb7f 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -59,6 +59,7 @@ let rec cases_pattern_fold_names f a = function
   | CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat
   | CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a
   | CPatPrim _ | CPatAtom _ -> a
+  | CPatCast _ -> assert false
 
 let ids_of_pattern_list =
   List.fold_left
@@ -92,6 +93,8 @@ let rec fold_local_binders g f n acc b = function
       f n (fold_local_binders g f n' acc b l) t
   | LocalRawDef ((_,na),t)::l ->
       f n (fold_local_binders g f (name_fold g na n) acc b l) t
+  | LocalPattern _::l ->
+      assert false
   | [] ->
       f n acc b
 
@@ -170,6 +173,7 @@ let split_at_annot bl na =
               (List.rev ans, LocalRawAssum (r, k, t) :: rest)
             end
 	| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
+        | LocalPattern _ :: rest -> assert false
 	| [] ->
             user_err_loc(loc,"",
 			 str "No parameter named " ++ Nameops.pr_id id ++ str".")
@@ -191,7 +195,9 @@ let map_local_binders f g e bl =
       LocalRawAssum(nal,k,ty) ->
         (map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl)
     | LocalRawDef((loc,na),ty) ->
-        (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) in
+        (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl)
+    | LocalPattern _ ->
+        assert false in
   let (e,rbl) = List.fold_left h (e,[]) bl in
   (e, List.rev rbl)