- Second pass on implementation of let pattern. Parse "let ' par [as x]?

  [in I] := t [return pred] in b", just as SSReflect does with let:. 
  Change implementation: no longer a separate AST node, just add a case_style
  annotation on Cases to indicate it (if ML was dependently typed we
  could ensure that LetPatternStyle Cases have only one term to be
  matched and one branch, alas...). This factors out most code and we lose
  no functionality (win ! win !). Add LetPat.v test suite.

- Slight improvement of inference of return clauses for dependent
  pattern matching. If matching a variable of non-dependent type
  under a tycon that mentions it while giving no return clause, the
  dependency will be automatically infered. Examples at the end of
  DepPat. Should get rid of most explicit returns under tycons.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10727 85f007b7-540e-0410-9357-904b9bb8a0f7

29 files changed, 249 insertions, 263 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 7385bf652f..aaa1b466da 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -224,11 +224,9 @@ let rec is_rec names =
 	  )
 	  b
     | RApp(_,f,args) -> List.exists (lookup names) (f::args)
-    | RCases(_,_,el,brl) -> 
+    | RCases(_,_,_,el,brl) -> 
 	List.exists (fun (e,_) -> lookup names e) el ||
 	  List.exists (lookup_br names) brl
-    | RLetPattern (_,(c,_),p) -> 
-	lookup names c || lookup_br names p
   and lookup_br names (_,idl,_,rt) = 
     let new_names = List.fold_right Idset.remove idl names in 
     lookup new_names rt
@@ -590,8 +588,8 @@ let rec add_args id new_args b =
   | CApp(loc,(pf,b),bl) -> 
       CApp(loc,(pf,add_args id new_args b), 
 	   List.map (fun (e,o) -> add_args id new_args e,o) bl)
-  | CCases(loc,b_option,cel,cal) -> 
-      CCases(loc,Option.map (add_args id new_args) b_option,
+  | CCases(loc,sty,b_option,cel,cal) -> 
+      CCases(loc,sty,Option.map (add_args id new_args) b_option,
 	     List.map (fun (b,(na,b_option)) -> 
 			 add_args id new_args b,
 			 (na,Option.map (add_args id new_args) b_option)) cel, 
@@ -603,9 +601,6 @@ let rec add_args id new_args b =
 		add_args id new_args b2
 	       )
 		
-  | CLetPattern(loc,p,b,c) ->
-      CLetPattern(loc,p,add_args id new_args b,add_args id new_args c)
-
   | CIf(loc,b1,(na,b_option),b2,b3) -> 
       CIf(loc,add_args id new_args b1, 
 	  (na,Option.map (add_args id new_args) b_option),
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 9276898e18..08a97fd221 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -567,7 +567,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 		  funnames 
 		  avoid
 		  (mkRLetIn(new_n,t,mkRApp(new_b,args)))
-	    | RCases _ | RLambda _ | RIf _ | RLetTuple _ | RLetPattern _ -> 
+	    | RCases _ | RLambda _ | RIf _ | RLetTuple _ -> 
 		(* we have [(match e1, ...., en with ..... end) t1 tn]
 		   we first compute the result from the case and 
 		   then combine each of them with each of args one
@@ -627,14 +627,12 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_letin n) v_res b_res
-    | RCases(_,_,el,brl) -> 
+    | RCases(_,_,_,el,brl) -> 
 	(* we create the discrimination function 
 	   and treat the case itself 
 	*)
 	let make_discr = make_discr_match brl in 
 	build_entry_lc_from_case env funnames make_discr el brl avoid
-    | RLetPattern (loc,c,p) -> 
-	build_entry_lc env funnames avoid (RCases (loc, None, [c], [p]))
     | RIf(_,b,(na,e_option),lhs,rhs) -> 
 	let b_as_constr = Pretyping.Default.understand Evd.empty env b in
 	let b_typ = Typing.type_of env Evd.empty b_as_constr in 
@@ -1021,7 +1019,7 @@ let rec compute_cst_params relnames params = function
   | RLambda(_,_,_,t,b) | RProd(_,_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> 
       let t_params = compute_cst_params relnames params t in 
       compute_cst_params relnames t_params b
-  | RCases _ | RLetPattern _ -> 
+  | RCases _ ->
       params  (* If there is still cases at this point they can only be 
 		 discriminitation ones *)
   | RSort _ -> params
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index c9341ba998..92396af590 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -15,7 +15,7 @@ let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl)
 let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b)
 let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b)
 let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
-let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
+let mkRCases(rto,l,brl) = RCases(dummy_loc,Term.RegularStyle,rto,l,brl)
 let mkRSort s = RSort(dummy_loc,s)
 let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
 let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
@@ -163,14 +163,12 @@ let change_vars =
 		    change_vars mapping b, 
 		    change_vars new_mapping e
 		   )
-      | RCases(loc,infos,el,brl) -> 
-	  RCases(loc,
+      | RCases(loc,sty,infos,el,brl) -> 
+	  RCases(loc,sty,
 		 infos,
 		 List.map (fun (e,x) -> (change_vars mapping e,x)) el, 
 		 List.map (change_vars_br mapping) brl
 		)
-      | RLetPattern(loc, (e,x), br) ->
-	  RLetPattern(loc, (change_vars mapping e, x), change_vars_br mapping br)
       | RIf(loc,b,(na,e_option),lhs,rhs) -> 
 	  RIf(loc,
 	      change_vars mapping b,
@@ -348,13 +346,11 @@ let rec alpha_rt excluded rt =
 	let new_b = alpha_rt new_excluded new_b in 
 	let new_rto = Option.map (alpha_rt new_excluded) new_rto  in
 	RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
-    | RCases(loc,infos,el,brl) -> 
+    | RCases(loc,sty,infos,el,brl) -> 
 	let new_el = 
 	  List.map (function (rt,i) -> alpha_rt excluded rt, i) el 
 	in 
-	RCases(loc,infos,new_el,List.map (alpha_br excluded) brl) 
-    | RLetPattern(loc,(rt,i),br) -> 
-	RLetPattern(loc, (alpha_rt excluded rt, i), alpha_br excluded br) 
+	RCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl) 
     | RIf(loc,b,(na,e_o),lhs,rhs) -> 
 	RIf(loc,alpha_rt excluded b,
 	    (na,Option.map (alpha_rt excluded) e_o),
@@ -402,10 +398,9 @@ let is_free_in id =
 	    | _ -> true
 	in
 	is_free_in t || (check_in_b && is_free_in b)
-    | RCases(_,_,el,brl) ->
+    | RCases(_,_,_,el,brl) ->
 	(List.exists (fun (e,_) -> is_free_in e) el) ||
 	  List.exists is_free_in_br brl
-    | RLetPattern(_,(e,_),br) -> is_free_in e || is_free_in_br br
     | RLetTuple(_,nal,_,b,t) -> 
 	let check_in_nal = 
 	  not (List.exists (function Name id' -> id'= id | _ -> false) nal) 
@@ -499,14 +494,12 @@ let replace_var_by_term x_id term =
 		    replace_var_by_pattern def,
 		    replace_var_by_pattern b
 		   )
-      | RCases(loc,infos,el,brl) -> 
-	  RCases(loc,
+      | RCases(loc,sty,infos,el,brl) -> 
+	  RCases(loc,sty,
 		 infos,
 		 List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, 
 		 List.map replace_var_by_pattern_br brl
 		)
-      | RLetPattern(loc,(e,x),br) ->
-	  RLetPattern(loc,(replace_var_by_pattern e, x), replace_var_by_pattern_br br)
       | RIf(loc,b,(na,e_option),lhs,rhs) -> 
 	  RIf(loc, replace_var_by_pattern b,
 	      (na,Option.map replace_var_by_pattern e_option),
@@ -608,10 +601,8 @@ let ids_of_rawterm c =
       | RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc
       | RLetTuple (_,nal,(na,po),b,c) -> 
           List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
-      | RCases (loc,rtntypopt,tml,brchl) -> 
+      | RCases (loc,sty,rtntypopt,tml,brchl) -> 
 	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl)
-      | RLetPattern (loc,tm,(_,idl,patl,c)) -> 
-	  idl @ ids_of_rawterm [] c
       | RRec _ -> failwith "Fix inside a constructor branch"
       | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> []
   in
@@ -658,17 +649,12 @@ let zeta_normalize =
 		    zeta_normalize_term def,
 		    zeta_normalize_term b
 		   )
-      | RCases(loc,infos,el,brl) -> 
-	  RCases(loc,
+      | RCases(loc,sty,infos,el,brl) -> 
+	  RCases(loc,sty,
 		 infos,
 		 List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, 
 		 List.map zeta_normalize_br brl
 		)
-      | RLetPattern(loc,(e,x),br) -> 
-	  RLetPattern(loc,
-		     (zeta_normalize_term e,x),
-		     zeta_normalize_br br
-	  )
       | RIf(loc,b,(na,e_option),lhs,rhs) -> 
 	  RIf(loc, zeta_normalize_term b,
 	      (na,Option.map zeta_normalize_term e_option),
@@ -723,14 +709,10 @@ let expand_as =
       | RDynamic _ -> error "Not handled RDynamic"
       | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
       | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce)
-      | RCases(loc,po,el,brl) ->
-	  RCases(loc, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
+      | RCases(loc,sty,po,el,brl) ->
+	  RCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
 		List.map (expand_as_br map) brl)
-      | RLetPattern(loc,(rt,t),br) ->
-	  RLetPattern(loc, (expand_as map rt,t),
-		expand_as_br map br)
-	    
   and expand_as_br map (loc,idl,cpl,rt) = 
-    (loc,idl,cpl,    expand_as (List.fold_left add_as map cpl) rt)
+    (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
   in
   expand_as Idmap.empty 
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 16357fc472..39eaa0b98b 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -210,7 +210,7 @@ let rec depends_of_rawconstr rc acc = match rc with
   | RLambda (_, _, _, rct, rcb)
   | RProd   (_, _, _, rct, rcb)
   | RLetIn  (_, _, rct, rcb) -> depends_of_rawconstr rcb (depends_of_rawconstr rct acc)
-  | RCases  (_, rco, tmt, cc) ->
+  | RCases  (_, _, rco, tmt, cc) ->
       (* LEM TODO: handle the cc *)
       (Option.fold_right depends_of_rawconstr rco
          (list_union_map
@@ -221,13 +221,6 @@ let rec depends_of_rawconstr rc acc = match rc with
 	    acc))
   | RLetTuple (_,_,(_,rco),rc0,rc1) ->
      depends_of_rawconstr rc1 (depends_of_rawconstr rc0 (Option.fold_right depends_of_rawconstr rco acc))
-  | RLetPattern (_, tmt, cc) ->
-      (* LEM TODO: handle the cc *)
-      (fun (rc, pp) acc ->
-	 Option.fold_right (fun (_,ind,_,_) acc -> (IndRef ind)::acc) (snd pp)
-	   (depends_of_rawconstr rc acc))
-	tmt
-	acc
   | RIf (_, rcC, (_, rco), rcT, rcF) -> let dorc = depends_of_rawconstr in
       dorc rcF (dorc rcT (dorc rcF (dorc rcC (Option.fold_right dorc rco acc))))
   | RRec (_, _, _, rdla, rca0, rca1) -> let dorca = array_union_map depends_of_rawconstr in
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 2219e327ca..aa7a50dce2 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -360,8 +360,6 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CLambdaN(_,ll,b)-> CT_lambdac(xlate_binder_ne_list ll, xlate_formula b)
    | CLetIn(_, v, a, b) -> 
        CT_letin(CT_def(xlate_id_opt v, xlate_formula a), xlate_formula b)
-   | CLetPattern(_, v, a, b) -> 
-       error "TODO: xlate_formula let | pattern"
    | CAppExpl(_, (Some n, r), l) -> 
        let l', last = decompose_last l in
 	 CT_proj(xlate_formula last,
@@ -379,8 +377,8 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 		 (xlate_formula f, List.map xlate_formula_expl l'))
    | CApp(_, (_,f), l) -> 
        CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
-   | CCases (_, _, [], _) -> assert false
-   | CCases (_, ret_type, tm::tml, eqns)->
+   | CCases (_, _, _, [], _) -> assert false
+   | CCases (_, _, ret_type, tm::tml, eqns)->
        CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm,
 					   List.map xlate_matched_formula tml),
 		xlate_formula_opt ret_type,
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index dd776088cc..8d9bfdbc51 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -1070,7 +1070,7 @@ let (value_f:constr list -> global_reference -> constr) =
     in
     let fun_body = 
       RCases
-	(d0,None,
+	(d0,RegularStyle,None,
 	 [RApp(d0, RRef(d0,fterm), List.rev_map (fun x_id -> RVar(d0, x_id)) rev_x_id_l),
 	  (Anonymous,None)],
 	 [d0, [v_id], [PatCstr(d0,(ind_of_ref 
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 54ed30a5dc..5b8bb9c0f8 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -241,6 +241,7 @@ type pattern_matching_problem =
       history  : pattern_continuation;
       mat      : matrix;
       caseloc  : loc;
+      casestyle: case_style;
       typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment }
 
 (*--------------------------------------------------------------------------*
@@ -1263,7 +1264,7 @@ and match_current pb tomatch =
 	  let (pred,typ,s) =
 	    find_predicate pb.caseloc pb.env pb.isevars 
 	      pb.pred brtyps cstrs current indt pb.tomatch in
-	  let ci = make_case_info pb.env mind RegularStyle in
+	  let ci = make_case_info pb.env mind pb.casestyle in
 	  let case = mkCase (ci,nf_betaiota pred,current,brvals) in
 	  let inst = List.map mkRel deps in
 	  { uj_val = applist (case, inst);
@@ -2081,7 +2082,7 @@ let nf_evars_env evar_defs (env : env) : env =
     Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e')
      ~init:env' env
       
-let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
+let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
   (* We build the matrix of patterns and right-hand-side *)
   let matx = matx_of_eqns env eqns in
      
@@ -2151,6 +2152,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
 	  history  = start_history (List.length initial_pushed);
 	  mat      = matx;
 	  caseloc  = loc;
+	  casestyle= style;
 	  typing_function = typing_fun } in
 	
       let j = compile pb in
@@ -2180,6 +2182,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
 	      history  = start_history (List.length initial_pushed);
 	      mat      = matx;
 	      caseloc  = loc;
+	      casestyle= style;
 	      typing_function = typing_fun } in
 	    
 	  let j = compile pb in
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 730b12605e..d3edb6e3cd 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -488,22 +488,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  in
 	    { uj_val = v; uj_type = p }
 
-    | RLetPattern (loc, c, p) ->
-	(* Just use cases typing *)
-	let j = 
-	  pretype tycon env isevars lvar 
-	    (RCases (loc, None, [c], [p]))
-	in
-	  (* Change case info *)
-	let j' = match kind_of_term j.uj_val with
-	    Case (ci, po, c, br) ->
-	      let pp_info = { ci.ci_pp_info with style = LetPatternStyle } in
-		{ j with uj_val = mkCase ({ ci with ci_pp_info = pp_info }, po, c, br) }
-	  | _ -> j
-	in j'
-
-    | RCases (loc,po,tml,eqns) ->
-	Cases.compile_cases loc
+    | RCases (loc,sty,po,tml,eqns) ->
+	Cases.compile_cases loc sty
 	  ((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
 	  tycon env (* loc *) (po,tml,eqns)
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index eb69e12257..11cd87763f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -195,7 +195,7 @@ let rec check_same_type ty1 ty2 =
       List.iter2 (fun (a1,e1) (a2,e2) ->
                     if e1<>e2 then failwith "not same expl";
                     check_same_type a1 a2) al1 al2
-  | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) ->
+  | CCases(_,_,_,a1,brl1), CCases(_,_,_,a2,brl2) ->
       List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2;
       List.iter2 (fun (_,pl1,r1) (_,pl2,r2) ->
         List.iter2 (located_iter2 (List.iter2 check_same_pattern)) pl1 pl2;
@@ -264,7 +264,7 @@ let rec same_raw c d =
   | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) ->
       if na1 <> na2 then failwith "RLetIn";
       same_raw t1 t2; same_raw m1 m2
-  | RCases(_,_,c1,b1), RCases(_,_,c2,b2) ->
+  | RCases(_,_,_,c1,b1), RCases(_,_,_,c2,b2) ->
       List.iter2
         (fun (t1,(al1,oind1)) (t2,(al2,oind2)) ->
           same_raw t1 t2;
@@ -690,7 +690,7 @@ let rec extern inctx scopes vars r =
       let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
       CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
 
-  | RCases (loc,rtntypopt,tml,eqns) ->
+  | RCases (loc,sty,rtntypopt,tml,eqns) ->
       let vars' = 
 	List.fold_right (name_fold Idset.add)
 	  (cases_predicate_names tml) vars in
@@ -713,7 +713,7 @@ let rec extern inctx scopes vars r =
 	  let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in
 	  (extern_typ scopes vars t)) x))) tml in
       let eqns = List.map (extern_eqn (rtntypopt<>None) scopes vars) eqns in 
-      CCases (loc,rtntypopt',tml,eqns)
+      CCases (loc,sty,rtntypopt',tml,eqns)
 
   | RLetTuple (loc,nal,(na,typopt),tm,b) ->
       CLetTuple (loc,nal,
@@ -722,15 +722,6 @@ let rec extern inctx scopes vars r =
         sub_extern false scopes vars tm,
         extern false scopes (List.fold_left add_vname vars nal) b)
 
-  | RLetPattern (loc,(tm,_), eqn) ->
-      let p, c = 
-	match extern_eqn false scopes vars eqn with
-	    (loc,[loc',[p]], c) -> p,c
-	  | _ -> assert false
-      in
-      let t = extern inctx scopes vars tm in
-	CLetPattern(loc, p, t, c)
-
   | RIf (loc,c,(na,typopt),b1,b2) ->
       CIf (loc,sub_extern false scopes vars c,
         (Option.map (fun _ -> na) typopt,
@@ -948,7 +939,7 @@ let rec raw_of_pat env = function
       let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in
       RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b)
   | PCase (_,PMeta None,tm,[||]) ->
-      RCases (loc,None,[raw_of_pat env tm,(Anonymous,None)],[])
+      RCases (loc,RegularStyle,None,[raw_of_pat env tm,(Anonymous,None)],[])
   | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) ->
       let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
       let brns = Array.to_list cstr_nargs in
@@ -960,7 +951,7 @@ let rec raw_of_pat env = function
 	else 
 	  let nparams,n = Option.get ind_nargs in
 	  return_type_of_predicate ind nparams n (raw_of_pat env p) in
-      RCases (loc,rtn,[raw_of_pat env tm,indnames],mat)
+      RCases (loc,RegularStyle,rtn,[raw_of_pat env tm,indnames],mat)
   | PFix f -> Detyping.detype false [] env (mkFix f)
   | PCoFix c -> Detyping.detype false [] env (mkCoFix c)
   | PSort s -> RSort (loc,s)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ce445c3f6d..9e962267db 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -901,7 +901,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
           (* Now compact "(f args') args" *)
 	  | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
 	  | _ -> RApp (loc, c, args))
-    | CCases (loc, rtnpo, tms, eqns) ->
+    | CCases (loc, sty, rtnpo, tms, eqns) ->
         let tms,env' = List.fold_right
           (fun citm (inds,env) ->
 	    let (tm,ind),nal = intern_case_item env citm in
@@ -909,7 +909,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	  tms ([],env) in
         let rtnpo = Option.map (intern_type env') rtnpo in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
-	RCases (loc, rtnpo, tms, List.flatten eqns')
+	RCases (loc, sty, rtnpo, tms, List.flatten eqns')
     | CLetTuple (loc, nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
         let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
@@ -917,11 +917,6 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let p' = Option.map (intern_type env'') po in
         RLetTuple (loc, nal, (na', p'), b',
                    intern (List.fold_left (push_name_env lvar) env nal) c)
-    | CLetPattern (loc, p, c, b) ->
-	let loc' = cases_pattern_expr_loc p in
-	let (tm,ind), nal = intern_case_item env (c,(None,None)) in
-	let eqn' = intern_eqn 1 env (loc, [loc',[p]], b) in
-	RLetPattern (loc, (tm,ind), List.hd eqn')
     | CIf (loc, c, (na,po), b1, b2) ->
 	let env' = reset_tmp_scope env in
         let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 082db5a390..f49c42a55d 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -57,15 +57,13 @@ let rec unloc = function
   | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c)
   | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c)
   | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
-  | RCases (_,rtntypopt,tml,pl) ->
-      RCases (dummy_loc,
+  | RCases (_,sty,rtntypopt,tml,pl) ->
+      RCases (dummy_loc,sty,
         (Option.map unloc rtntypopt),
 	List.map (fun (tm,x) -> (unloc tm,x)) tml,
         List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
   | RLetTuple (_,nal,(na,po),b,c) ->
       RLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c)
-  | RLetPattern (_,(tm,x),(_,idl,p,c)) -> 
-      RLetPattern (dummy_loc,(unloc tm,x),(dummy_loc,idl,p,unloc c))
   | RIf (_,c,(na,po),b1,b2) ->
       RIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2)
   | RRec (_,fk,idl,bl,tyl,bv) ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c9a33c7eba..05a1465ac8 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -37,7 +37,7 @@ type aconstr =
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
-  | ACases of aconstr option *
+  | ACases of case_style * aconstr option *
       (aconstr * (name * (inductive * int * name list) option)) list *
       (cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
@@ -79,7 +79,7 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let e,na = name_fold_map g e na in RProd (loc,na,Explicit,f e ty,f e c)
   | ALetIn (na,b,c) ->
       let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c)
-  | ACases (rtntypopt,tml,eqnl) ->
+  | ACases (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
@@ -94,7 +94,7 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
 	let ((idl,e),patl) =
 	  list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
 	(loc,idl,patl,f e rhs)) eqnl in
-      RCases (loc,Option.map (f e') rtntypopt,tml',eqnl')
+      RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
   | ALetTuple (nal,(na,po),b,c) ->
       let e,nal = list_fold_map (name_fold_map g) e nal in 
       let e,na = name_fold_map g e na in
@@ -138,9 +138,9 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
   | RHole _, RHole _ -> true
   | RSort (_,s1), RSort (_,s2) -> s1 = s2
   | (RLetIn _ | RCases _ | RRec _ | RDynamic _
-    | RPatVar _ | REvar _ | RLetTuple _ | RLetPattern _ | RIf _ | RCast _),_
+    | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
   | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
-      | RPatVar _ | REvar _ | RLetTuple _ | RLetPattern _ | RIf _ | RCast _)
+      | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
       -> error "Unsupported construction in recursive notations"
   | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _
       -> false
@@ -183,9 +183,9 @@ let aconstr_and_vars_of_rawconstr a =
   | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
   | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
   | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
-  | RCases (_,rtntypopt,tml,eqnl) ->
+  | RCases (_,sty,rtntypopt,tml,eqnl) ->
       let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in
-      ACases (Option.map aux rtntypopt,
+      ACases (sty,Option.map aux rtntypopt,
         List.map (fun (tm,(na,x)) ->
 	  add_name found na;
 	  Option.iter
@@ -196,7 +196,6 @@ let aconstr_and_vars_of_rawconstr a =
       add_name found na;
       List.iter (add_name found) nal;
       ALetTuple (nal,(na,Option.map aux po),aux b,aux c)
-  | RLetPattern (loc, c, p) -> error "TODO: aconstr of letpattern"
   | RIf (loc,c,(na,po),b1,b2) ->
       add_name found na;
       AIf (aux c,(na,Option.map aux po),aux b1,aux b2)
@@ -208,8 +207,7 @@ let aconstr_and_vars_of_rawconstr a =
   | RRef (_,r) -> ARef r
   | RPatVar (_,(_,n)) -> APatVar n
   | RDynamic _ | RRec _ | REvar _ ->
-      error "Fixpoints, cofixpoints, existential variables and pattern-matching  not \
-allowed in abbreviatable expressions"
+      error "Fixpoints, cofixpoints and existential variables not allowed in abbreviatable expressions"
 
   (* Recognizing recursive notations *)
   and terminator_of_pat f1 ll1 lr1 = function
@@ -305,7 +303,7 @@ let rec subst_aconstr subst bound raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  ALetIn (n,r1',r2')
 
-  | ACases (rtntypopt,rl,branches) -> 
+  | ACases (sty,rtntypopt,rl,branches) -> 
       let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt
       and rl' = list_smartmap
         (fun (a,(n,signopt) as x) -> 
@@ -325,7 +323,7 @@ let rec subst_aconstr subst bound raw =
       in
         if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' &
           rl' == rl && branches' == branches then raw else
-          ACases (rtntypopt',rl',branches')
+          ACases (sty,rtntypopt',rl',branches')
 
   | ALetTuple (nal,(na,po),b,c) ->
       let po' = Option.smartmap (subst_aconstr subst bound) po
@@ -447,8 +445,9 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
      match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
   | RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) ->
      match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
-  | RCases (_,rtno1,tml1,eqnl1), ACases (rtno2,tml2,eqnl2) 
-      when List.length tml1 = List.length tml2
+  | RCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2) 
+      when sty1 = sty2
+	 & List.length tml1 = List.length tml2
 	 & List.length eqnl1 = List.length eqnl2 ->
       let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in
       let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in
@@ -559,12 +558,11 @@ type constr_expr =
   | CAppExpl of loc * (proj_flag * reference) * constr_expr list
   | CApp of loc * (proj_flag * constr_expr) * 
       (constr_expr * explicitation located option) list
-  | CCases of loc * constr_expr option *
+  | CCases of loc * case_style * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
       (loc * cases_pattern_expr list located list * constr_expr) list
   | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
-  | CLetPattern of loc * cases_pattern_expr * constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)
       * constr_expr * constr_expr
   | CHole of loc * Evd.hole_kind option
@@ -577,7 +575,6 @@ type constr_expr =
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
-
 and fixpoint_expr =
     identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
@@ -632,9 +629,8 @@ let constr_loc = function
   | CLetIn (loc,_,_,_) -> loc
   | CAppExpl (loc,_,_) -> loc
   | CApp (loc,_,_) -> loc
-  | CCases (loc,_,_,_) -> loc
+  | CCases (loc,_,_,_,_) -> loc
   | CLetTuple (loc,_,_,_,_) -> loc
-  | CLetPattern (loc,_,_,_) -> loc
   | CIf (loc,_,_,_,_) -> loc
   | CHole (loc, _) -> loc
   | CPatVar (loc,_) -> loc
@@ -726,7 +722,7 @@ let fold_constr_expr_with_binders g f n acc = function
   | CDelimiters (loc,_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _  | CRef _ ->
       acc
-  | CCases (loc,rtnpo,al,bl) ->
+  | CCases (loc,sty,rtnpo,al,bl) ->
       let ids = ids_of_cases_tomatch al in
       let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in
       let acc = List.fold_left (f n) acc (List.map fst al) in
@@ -736,10 +732,6 @@ let fold_constr_expr_with_binders g f n acc = function
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let n' = List.fold_right (name_fold g) nal n in
       f (Option.fold_right (name_fold g) ona n') (f n acc b) c
-  | CLetPattern (loc,p,b,c) ->
-      let acc = f n acc b in
-      let ids = cases_pattern_fold_names Idset.add Idset.empty p in
-	f (Idset.fold g ids n) acc c
   | CIf (_,c,(ona,po),b1,b2) ->
       let acc = f n (f n (f n acc b1) b2) c in
       Option.fold_left (f (Option.fold_right (name_fold g) ona n)) acc po
@@ -841,19 +833,16 @@ let map_constr_expr_with_binders g f e = function
   | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _ 
   | CPrim _ | CDynamic _ | CRef _ as x -> x
-  | CCases (loc,rtnpo,a,bl) ->
+  | CCases (loc,sty,rtnpo,a,bl) ->
       (* TODO: apply g on the binding variables in pat... *)
       let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
       let ids = ids_of_cases_tomatch a in
       let po = Option.map (f (List.fold_right g ids e)) rtnpo in
-      CCases (loc, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
+      CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let e' = List.fold_right (name_fold g) nal e in
       let e'' = Option.fold_right (name_fold g) ona e in
       CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c)
-  | CLetPattern (loc, p, b, c) -> 
-      (* TODO: apply g on the binding variables in pat... *)
-      CLetPattern (loc, p, f e b,f e c)
   | CIf (loc,c,(ona,po),b1,b2) ->
       let e' = Option.fold_right (name_fold g) ona e in
       CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 26805aa13e..4e46d95902 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -33,7 +33,7 @@ type aconstr =
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
-  | ACases of aconstr option *
+  | ACases of case_style * aconstr option *
       (aconstr * (name * (inductive * int * name list) option)) list *
       (cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
@@ -117,13 +117,12 @@ type constr_expr =
   | CLetIn of loc * name located * constr_expr * constr_expr
   | CAppExpl of loc * (proj_flag * reference) * constr_expr list
   | CApp of loc * (proj_flag * constr_expr) * 
-        (constr_expr * explicitation located option) list
-  | CCases of loc * constr_expr option *
+      (constr_expr * explicitation located option) list
+  | CCases of loc * case_style * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
       (loc * cases_pattern_expr list located list * constr_expr) list
   | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
-  | CLetPattern of loc * cases_pattern_expr * constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)
       * constr_expr * constr_expr
   | CHole of loc * Evd.hole_kind option
diff --git a/kernel/term.mli b/kernel/term.mli
index 8d6c20a353..70c5ceded9 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -439,8 +439,8 @@ val noccurn : int -> constr -> bool
 val noccur_between : int -> int -> constr -> bool
 
 (* Checking function for terms containing existential- or
-   meta-variables.  The function [noccur_with_meta] considers only
-   meta-variable applied to some terms (intented to be its local
+   meta-variables.  The function [noccur_with_meta] does not consider
+   meta-variables applied to some terms (intented to be its local
    context) (for existential variables, it is necessarily the case) *)
 val noccur_with_meta : int -> int -> constr -> bool
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 423ade8b6d..0e7c92a6ce 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -125,6 +125,8 @@ let ident_eq =
               | _ -> raise Stream.Failure)
         | _ -> raise Stream.Failure)
 
+let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
+
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
   constr_pattern lconstr_pattern Constr.ident
@@ -228,15 +230,16 @@ GEXTEND Gram
 	  ":="; c1 = operconstr LEVEL "200"; "in";
           c2 = operconstr LEVEL "200" ->
           CLetTuple (loc,List.map snd lb,po,c1,c2)
-      | "let"; "|"; p=pattern; ":="; c1 = operconstr LEVEL "200";
+      | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
           "in"; c2 = operconstr LEVEL "200" ->
-	    CLetPattern (loc, p, c1, c2)
-      | "dest"; c1 = operconstr LEVEL "200";
-	  "as"; p=pattern; 
+	    CCases (loc, LetPatternStyle, None, [(c1,(None,None))], [(loc, [(loc,[p])], c2)])
+      | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; 
+	  rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
+	    CCases (loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, None))], [(loc, [(loc, [p])], c2)])
+      | "let"; "'"; p=pattern; "in"; t = operconstr LEVEL "200"; 
+	  ":="; c1 = operconstr LEVEL "200"; rt = case_type;
           "in"; c2 = operconstr LEVEL "200" ->
-	    let loc' = cases_pattern_expr_loc p in
-              CCases (loc, None, [(c1, (None, None))],
-                     [loc, [loc',[p]], c2])
+	    CCases (loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, Some t))], [(loc, [(loc, [p])], c2)])
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
@@ -283,7 +286,7 @@ GEXTEND Gram
 (*   ; *)
   match_constr:
     [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
-        br=branches; "end" -> CCases(loc,ty,ci,br) ] ]
+        br=branches; "end" -> CCases(loc,RegularStyle,ty,ci,br) ] ]
   ;
   case_item:
     [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ]
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 47725cbd65..a9f3fd487c 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -171,7 +171,7 @@ let rec interp_xml_constr = function
       let mat = simple_cases_matrix_of_branches ind brns brs in
       let nparams,n = compute_inductive_nargs ind in
       let nal,rtn = return_type_of_predicate ind nparams n p in
-      RCases (loc,rtn,[tm,nal],mat)
+      RCases (loc,RegularStyle,rtn,[tm,nal],mat)
   | XmlTag (loc,"MUTIND",al,[]) ->
       RRef (loc, IndRef (get_xml_inductive al))
   | XmlTag (loc,"MUTCONSTRUCT",al,[]) ->
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 7d0d085938..21c5a343b4 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -434,27 +434,16 @@ let tm_clash = function
       -> Some id
   | _ -> None
 
-let pr_case_item pr (tm,(na,indnalopt)) =
-  hov 0 (pr (lcast,E) tm ++
-(*
-  (match na with
-    | Name id when not (is_var id tm) -> spc () ++ str "as " ++  pr_id id
-    | Anonymous when tm_clash (tm,indnalopt) <> None ->
-	(* hide [tm] name to avoid conflicts *)
-	spc () ++ str "as _" (* ++ pr_id (Option.get (tm_clash (tm,indnalopt)))*)
-    | _ -> mt ()) ++
-*)
+let pr_asin pr (na,indnalopt) =
   (match na with (* Decision of printing "_" or not moved to constrextern.ml *)
     | Some na -> spc () ++ str "as " ++  pr_name na
     | None -> mt ()) ++
   (match indnalopt with
     | None -> mt ()
-(*
-    | Some (_,ind,nal) ->
-        spc () ++ str "in " ++ 
-        hov 0 (pr_reference ind ++ prlist (pr_arg pr_name) nal))
-*)
-    | Some t -> spc () ++ str "in " ++ pr lsimple t))
+    | Some t -> spc () ++ str "in " ++ pr lsimple t)
+    
+let pr_case_item pr (tm,asin) =
+  hov 0 (pr (lcast,E) tm ++ pr_asin pr asin)
 
 let pr_case_type pr po =
   match po with
@@ -551,15 +540,24 @@ let rec pr sep inherited a =
       else
 	p, lproj
   | CApp (_,(None,a),l) -> pr_app (pr mt) a l, lapp
-  | CCases (_,rtntypopt,c,eqns) ->
+  | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) ->
+      hv 0 (
+	str "let '" ++ 
+	  hov 0 (pr_patt ltop p ++ 
+		 pr_asin (pr_dangling_with_for mt) asin ++
+		 str " :=" ++ pr spc ltop c ++ 
+		 pr_case_type (pr_dangling_with_for mt) rtntypopt ++
+		 str " in" ++ pr spc ltop b)),
+	lletpattern
+  | CCases(_,_,rtntypopt,c,eqns) ->
       v 0
         (hv 0 (str "match" ++ brk (1,2) ++
-	  hov 0 (
-	    prlist_with_sep sep_v
-              (pr_case_item (pr_dangling_with_for mt)) c
-            ++ pr_case_type (pr_dangling_with_for mt) rtntypopt) ++
-	spc () ++ str "with") ++
-        prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"),
+		  hov 0 (
+		    prlist_with_sep sep_v
+		      (pr_case_item (pr_dangling_with_for mt)) c
+		    ++ pr_case_type (pr_dangling_with_for mt) rtntypopt) ++
+		  spc () ++ str "with") ++
+		  prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"),
       latom
   | CLetTuple (_,nal,(na,po),c,b) ->
       hv 0 (
@@ -571,11 +569,6 @@ let rec pr sep inherited a =
                pr spc ltop c ++ str " in") ++
         pr spc ltop b),
       lletin
-  | CLetPattern (_, p, c, b) ->
-      hv 0 (
-	str "let| " ++ 
-	hov 0 (pr_patt ltop p ++ str " :=" ++ pr spc ltop c ++ str " in") ++
-	pr spc ltop b), lletpattern
   | CIf (_,c,(na,po),b1,b2) ->
       (* On force les parenthèses autour d'un "if" sous-terme (même si le
 	 parsing est lui plus tolérant) *)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index b5ad753afc..922c7af163 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -153,7 +153,7 @@ let rec mlexpr_of_constr = function
   | Topconstr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
   | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>
-  | Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
+  | Topconstr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >>
   | Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
   | Topconstr.CNotation(_,ntn,l) ->
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b7317b5be0..e1c5beeea2 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -65,7 +65,7 @@ let error_needs_inversion env x t =
 
 module type S = sig
   val compile_cases :
-    loc ->
+    loc -> case_style ->
     (type_constraint -> env -> rawconstr -> unsafe_judgment) *
       Evd.evar_defs ref ->
     type_constraint -> 
@@ -275,13 +275,14 @@ let push_history_pattern n current cont =
 
 *)
 type pattern_matching_problem =
-    { env      : env;
-      evdref   : Evd.evar_defs ref;
-      pred     : predicate_signature option;
-      tomatch  : tomatch_stack;
-      history  : pattern_continuation;
-      mat      : matrix;
-      caseloc  : loc;
+    { env       : env;
+      evdref    : Evd.evar_defs ref;
+      pred      : predicate_signature option;
+      tomatch   : tomatch_stack;
+      history   : pattern_continuation;
+      mat       : matrix;
+      caseloc   : loc;
+      casestyle : case_style;
       typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment }
 
 (*--------------------------------------------------------------------------*
@@ -1275,7 +1276,7 @@ and match_current pb tomatch =
 	  let (pred,typ,s) =
 	    find_predicate pb.caseloc pb.env pb.evdref 
 	      pb.pred brtyps cstrs current indt pb.tomatch in
-	  let ci = make_case_info pb.env mind RegularStyle in
+	  let ci = make_case_info pb.env mind pb.casestyle in
 	  let case = mkCase (ci,nf_betaiota pred,current,brvals) in
 	  let inst = List.map mkRel deps in
 	  { uj_val = applist (case, inst);
@@ -1504,7 +1505,7 @@ let extract_arity_signature env0 tomatchl tmsign =
 	    | Some (loc,_,_,_) -> 
  	    user_err_loc (loc,"",
 	    str "Unexpected type annotation for a term of non inductive type"))
-      | IsInd (_,IndType(indf,realargs)) ->
+      | IsInd (term,IndType(indf,realargs)) ->
           let indf' = lift_inductive_family n indf in
 	  let (ind,params) = dest_ind_family indf' in
 	  let nrealargs = List.length realargs in
@@ -1519,6 +1520,14 @@ let extract_arity_signature env0 tomatchl tmsign =
 		  List.rev realnal
 	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
 	  let arsign = fst (get_arity env0 indf') in
+(* 	  let na =  *)
+(* 	    match na with  *)
+(* 	      | Name _ -> na *)
+(* 	      | Anonymous -> *)
+(* 		  match kind_of_term term with *)
+(* 		    | Rel n -> pi1 (lookup_rel n (Environ.rel_context env0)) *)
+(* 		    | _ -> Anonymous *)
+(* 	  in *)
 	  (na,None,build_dependent_inductive env0 indf')
 	  ::(List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign) in
   let rec buildrec n = function
@@ -1537,6 +1546,34 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
           j
     | None -> j
 
+(* We put the tycon inside the arity signature, possibly discovering dependencies. *)
+
+let prepare_predicate_from_arsign_tycon loc env evdref tomatchs sign arsign c =
+  let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
+  let subst, len = 
+    List.fold_left2 (fun (subst, len) (tm, tmtype) sign ->
+      let signlen = List.length sign in
+	match kind_of_term tm with
+	  | Rel n when dependent tm c 
+		&& signlen = 1 (* The term to match is not of a dependent type itself *) ->
+	      ((n, len) :: subst, len - signlen)
+	  | _ -> (subst, len - signlen))
+      ([], nar) tomatchs arsign
+  in
+  let rec predicate lift c =
+    match kind_of_term c with
+      | Rel n when n > lift -> 
+	  (try 
+	      (* Make the predicate dependent on the matched variable *)
+	      let idx = List.assoc (n - lift) subst in
+		mkRel (idx + lift)
+	    with Not_found -> 
+	      (* A variable that is not matched, lift over the arsign. *)
+	      mkRel (n + nar))
+      | _ ->
+	  map_constr_with_binders succ predicate lift c 
+  in predicate 0 c
+
 
 (* Builds the predicate. If the predicate is dependent, its context is
  * made of 1+nrealargs assumptions for each matched term in an inductive
@@ -1545,7 +1582,8 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
 
  * Each matched terms are independently considered dependent or not.
 
- * A type constraint but no annotation case: it is assumed non dependent.
+ * A type constraint but no annotation case: we try to specialize the
+ * tycon to make the predicate if it is not closed.
  *)
 
 let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function
@@ -1553,9 +1591,23 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function
   | None ->
       (match tycon with
        | Some (None, t) ->
-	   let names,pred = 
-	     prepare_predicate_from_tycon loc false env evdref tomatchs sign t 
-	   in Some (build_initial_predicate false names pred)
+	   if noccur_with_meta 0 max_int t then
+	     let names,pred =
+	       prepare_predicate_from_tycon loc false env evdref tomatchs sign t
+	     in
+	       Some (build_initial_predicate false names pred)
+	   else
+	     let arsign = extract_arity_signature env tomatchs sign in
+	     let env' = List.fold_right push_rels arsign env in
+	     let names = List.rev (List.map (List.map pi1) arsign) in
+	     let pred = prepare_predicate_from_arsign_tycon loc env' evdref tomatchs sign arsign t in
+	       if eq_constr pred t then
+		 let names,pred =
+		   prepare_predicate_from_tycon loc false env evdref tomatchs sign t
+		 in
+		   Some (build_initial_predicate false names pred)
+	       else
+		 Some (build_initial_predicate true names pred)
        | _ -> None)
 
   (* Some type annotation *)
@@ -1577,7 +1629,7 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
   
-let compile_cases loc (typing_fun, evdref) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)=
+let compile_cases loc style (typing_fun, evdref) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)=
   
   (* We build the matrix of patterns and right-hand-side *)
   let matx = matx_of_eqns env tomatchl eqns in
@@ -1596,13 +1648,14 @@ let compile_cases loc (typing_fun, evdref) (tycon : Evarutil.type_constraint) en
   let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
     
   let pb =
-    { env      = env;
-      evdref   = evdref;
-      pred     = pred;
-      tomatch  = initial_pushed;
-      history  = start_history (List.length initial_pushed);
-      mat      = matx;
-      caseloc  = loc;
+    { env       = env;
+      evdref    = evdref;
+      pred      = pred;
+      tomatch   = initial_pushed;
+      history   = start_history (List.length initial_pushed);
+      mat       = matx;
+      caseloc   = loc;
+      casestyle = style;
       typing_function = typing_fun } in
     
   let j = compile pb in
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index d105ca2d0f..a2015c2b17 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -50,7 +50,7 @@ val error_needs_inversion : env -> constr -> types -> 'a
 
 module type S = sig
   val compile_cases :
-    loc ->
+    loc -> case_style ->
     (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref ->
     type_constraint -> 
     env -> rawconstr option * tomatch_tuples * cases_clauses ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 34e6945584..164043cf7c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -349,8 +349,6 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
       let bl' = Array.map detype bl in
       let (nal,d) = it_destRLambda_or_LetIn_names consnargsl.(0) bl'.(0) in
       RLetTuple (dl,nal,(alias,pred),tomatch,d)
-  | LetPatternStyle when List.length eqnl = 1 -> (* If irrefutable due to some inversion, print as match *) 
-      RLetPattern (dl,(tomatch,(alias,aliastyp)),List.hd eqnl)
   | IfStyle when aliastyp = None ->
       let bl' = Array.map detype bl in
       let nondepbrs =
@@ -359,9 +357,9 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
 	RIf (dl,tomatch,(alias,pred),
              Option.get nondepbrs.(0),Option.get nondepbrs.(1))
       else
-	RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl)
+	RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
   | _ ->
-      RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl)
+      RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
 let detype_sort = function
   | Prop c -> RProp c
@@ -605,7 +603,7 @@ let rec subst_rawconstr subst raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  RLetIn (loc,n,r1',r2')
 
-  | RCases (loc,rtno,rl,branches) -> 
+  | RCases (loc,sty,rtno,rl,branches) -> 
       let rtno' = Option.smartmap (subst_rawconstr subst) rtno
       and rl' = list_smartmap (fun (a,x as y) ->
         let a' = subst_rawconstr subst a in
@@ -625,7 +623,7 @@ let rec subst_rawconstr subst raw =
 			branches
       in
 	if rtno' == rtno && rl' == rl && branches' == branches then raw else
-	  RCases (loc,rtno',rl',branches')
+	  RCases (loc,sty,rtno',rl',branches')
 
   | RLetTuple (loc,nal,(na,po),b,c) ->
       let po' = Option.smartmap (subst_rawconstr subst) po
@@ -633,28 +631,6 @@ let rec subst_rawconstr subst raw =
       and c' = subst_rawconstr subst c in
 	if po' == po && b' == b && c' == c then raw else
           RLetTuple (loc,nal,(na,po'),b',c')
-
-  | RLetPattern (loc, (a,x as c), (loc',idl,cpl,r as branch)) ->
-      let c' = 
-	let a' = subst_rawconstr subst a in
-        let (n,topt) = x in 
-        let topt' = Option.smartmap
-          (fun (loc,(sp,i),x,y as t) ->
-            let sp' = subst_kn subst sp in
-              if sp == sp' then t else (loc,(sp',i),x,y))
-	  topt 
-	in
-          if a == a' && topt == topt' then c else (a',(n,topt'))
-      in
-      let p' = 
-	let cpl' =
-	  list_smartmap (subst_cases_pattern subst) cpl
-	and r' = subst_rawconstr subst r in
-	  if cpl' == cpl && r' == r then branch else
-	    (loc',idl,cpl',r')
-      in 
-	if c' == c && p' == branch then raw else
-	  RLetPattern (loc, c', p')
 	        
   | RIf (loc,c,(na,po),b1,b2) ->
       let po' = Option.smartmap (subst_rawconstr subst) po
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 845f9fae1f..90a3728ebb 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -245,7 +245,7 @@ let rec pat_of_raw metas vars = function
       let c = List.fold_left mkRLambda c nal in
       PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b,
              [|pat_of_raw metas vars c|])
-  | RCases (loc,p,[c,(na,indnames)],brs) ->
+  | RCases (loc,sty,p,[c,(na,indnames)],brs) ->
       let pred,ind_nargs, ind = match p,indnames with
 	| Some p, Some (_,ind,n,nal) ->
 	    rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)),
@@ -259,7 +259,7 @@ let rec pat_of_raw metas vars = function
 	Array.init (List.length brs) (pat_of_raw_branch loc metas vars ind brs)
       in
       let cstr_nargs,brs = (Array.map fst cbrs, Array.map snd cbrs) in
-      PCase ((RegularStyle,cstr_nargs,ind,ind_nargs), pred,
+      PCase ((sty,cstr_nargs,ind,ind_nargs), pred,
              pat_of_raw metas vars c, brs)
              
   | r ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f9fcdb7b63..83381710d3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -582,23 +582,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	      mkCase (ci, pred, cj.uj_val, [|b1;b2|])
 	  in
 	    { uj_val = v; uj_type = p }
-
-    | RLetPattern (loc, c, p) ->
-	(* Just use cases typing *)
-	let j = 
-	  pretype tycon env evdref lvar 
-	    (RCases (loc, None, [c], [p]))
-	in 
-	(* Change case info *)
-	let j' = match kind_of_term j.uj_val with
-	    Case (ci, po, c, br) ->
-	      let pp_info = { ci.ci_pp_info with style = LetPatternStyle } in
-		{ j with uj_val = mkCase ({ ci with ci_pp_info = pp_info }, po, c, br) }
-	  | _ -> j
-	in j'
 	
-    | RCases (loc,po,tml,eqns) ->
-	Cases.compile_cases loc
+    | RCases (loc,sty,po,tml,eqns) ->
+	Cases.compile_cases loc sty
 	  ((fun vtyc env -> pretype vtyc env evdref lvar),evdref)
 	  tycon env (* loc *) (po,tml,eqns)
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index e7f5de028f..fe48cd4fa7 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -62,10 +62,9 @@ type rawconstr =
   | RLambda of loc * name * binding_kind * rawconstr * rawconstr
   | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option * tomatch_tuples * cases_clauses
+  | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
-  | RLetPattern of loc * tomatch_tuple * cases_clause
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
   | RRec of loc * fix_kind * identifier array * rawdecl list array *
       rawconstr array * rawconstr array
@@ -115,14 +114,12 @@ let map_rawconstr f = function
   | RLambda (loc,na,bk,ty,c) -> RLambda (loc,na,bk,f ty,f c)
   | RProd (loc,na,bk,ty,c) -> RProd (loc,na,bk,f ty,f c)
   | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
-  | RCases (loc,rtntypopt,tml,pl) ->
-      RCases (loc,Option.map f rtntypopt,
+  | RCases (loc,sty,rtntypopt,tml,pl) ->
+      RCases (loc,sty,Option.map f rtntypopt,
         List.map (fun (tm,x) -> (f tm,x)) tml,
         List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl)
   | RLetTuple (loc,nal,(na,po),b,c) ->
       RLetTuple (loc,nal,(na,Option.map f po),f b,f c)
-  | RLetPattern (loc,(b,x),(loc',idl,p,c)) ->
-      RLetPattern (loc,(f b,x),(loc',idl,p,f c))
   | RIf (loc,c,(na,po),b1,b2) ->
       RIf (loc,f c,(na,Option.map f po),f b1,f b2)
   | RRec (loc,fk,idl,bl,tyl,bv) ->
@@ -177,14 +174,13 @@ let occur_rawconstr id =
     | RLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
-    | RCases (loc,rtntypopt,tml,pl) ->
+    | RCases (loc,sty,rtntypopt,tml,pl) ->
 	(occur_option rtntypopt)
         or (List.exists (fun (tm,_) -> occur tm) tml)
 	or (List.exists occur_pattern pl)
     | RLetTuple (loc,nal,rtntyp,b,c) -> 
 	occur_return_type rtntyp id
         or (occur b) or (not (List.mem (Name id) nal) & (occur c))
-    | RLetPattern (loc, (b, _), p) -> (occur b) or (occur_pattern p)
     | RIf (loc,c,rtntyp,b1,b2) -> 
 	occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
     | RRec (loc,fk,idl,bl,tyl,bv) ->
@@ -224,7 +220,7 @@ let free_rawvars  =
 	let vs' = vars bounded vs ty in 
 	let bounded' = add_name_to_ids bounded na in 
 	vars bounded' vs' c
-    | RCases (loc,rtntypopt,tml,pl) ->
+    | RCases (loc,sty,rtntypopt,tml,pl) ->
 	let vs1 = vars_option bounded vs rtntypopt in 
 	let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in 
 	List.fold_left (vars_pattern bounded) vs2 pl
@@ -233,7 +229,6 @@ let free_rawvars  =
 	let vs2 = vars bounded vs1 b in 
 	let bounded' = List.fold_left add_name_to_ids bounded nal in
 	vars bounded' vs2 c
-    | RLetPattern (loc, (c, _), p) -> vars_pattern bounded (vars bounded vs c) p
     | RIf (loc,c,rtntyp,b1,b2) -> 
 	let vs1 = vars_return_type bounded vs rtntyp in 
 	let vs2 = vars bounded vs1 c in 
@@ -285,8 +280,7 @@ let loc_of_rawconstr = function
   | RLambda (loc,_,_,_,_) -> loc
   | RProd (loc,_,_,_,_) -> loc
   | RLetIn (loc,_,_,_) -> loc
-  | RLetPattern (loc,_,_) -> loc
-  | RCases (loc,_,_,_) -> loc
+  | RCases (loc,_,_,_,_) -> loc
   | RLetTuple (loc,_,_,_,_) -> loc
   | RIf (loc,_,_,_,_) -> loc
   | RRec (loc,_,_,_,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 7b342c4115..ab67a0922b 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -66,10 +66,9 @@ type rawconstr =
   | RLambda of loc * name * binding_kind *  rawconstr * rawconstr
   | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option * tomatch_tuples * cases_clauses
+  | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
-  | RLetPattern of loc * tomatch_tuple * cases_clause
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
   | RRec of loc * fix_kind * identifier array * rawdecl list array *
       rawconstr array * rawconstr array
diff --git a/test-suite/success/LetPat.v b/test-suite/success/LetPat.v
new file mode 100644
index 0000000000..72c7cc1553
--- /dev/null
+++ b/test-suite/success/LetPat.v
@@ -0,0 +1,55 @@
+(* Simple let-patterns *)
+Variable A B : Type.
+
+Definition l1 (t : A * B * B) : A := let '(x, y, z) := t in x.
+Print l1.
+Definition l2 (t : (A * B) * B) : A := let '((x, y), z) := t in x.
+Definition l3 (t : A * (B * B)) : A := let '(x, (y, z)) := t in x.
+Print l3.
+
+Record someT (A : Type) := mkT { a : nat; b: A }.
+
+Definition l4 A (t : someT A) : nat := let 'mkT x y := t in x.
+Print l4.
+Print sigT.
+
+Definition l5 A (B : A -> Type) (t : sigT B) : B (projT1 t) := 
+  let 'existT x y := t return B (projT1 t) in y.
+
+Definition l6 A (B : A -> Type) (t : sigT B) : B (projT1 t) := 
+  let 'existT x y as t' := t return B (projT1 t') in y.
+
+Definition l7 A (B : A -> Type) (t : sigT B) : B (projT1 t) := 
+  let 'existT x y as t' in sigT _ := t return B (projT1 t') in y.
+
+Definition l8 A (B : A -> Type) (t : sigT B) : B (projT1 t) := 
+  match t with
+    existT x y => y
+  end.
+
+(** An example from algebra, using let' and inference of return clauses
+   to deconstruct contexts. *)
+
+Record a_category (A : Type) (hom : A -> A -> Type) := {  }.
+
+Definition category := { A : Type & { hom : A -> A -> Type & a_category A hom } }.
+
+Record a_functor (A : Type) (hom : A -> A -> Type) (C : a_category A hom) := {  }.
+
+Notation " x :& y " := (@existT _ _ x y) (right associativity, at level 55) : core_scope.
+
+Definition functor (c d : category) :=
+  let ' A :& homA :& CA := c in
+  let ' B :& homB :& CB := d in
+    A -> B.
+
+Definition identity_functor (c : category) : functor c c :=
+  let 'A :& homA :& CA := c in
+    fun x => x.
+
+Definition functor_composition (a b c : category) : functor a b -> functor b c -> functor a c := 
+  let ' (A :& homA :& CA) := a in
+  let ' (B :& homB :& CB) := b in
+  let ' (C :& homB :& CB) := c in
+    fun f g => 
+      fun x : A => g (f x).
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 0850237202..d215bccb9e 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -97,8 +97,8 @@ Program Instance unit_eqdec : ! EqDec unit eq :=
 Program Instance [ EqDec A eq, EqDec B eq ] => 
   prod_eqdec : ! EqDec (prod A B) eq :=
   equiv_dec x y := 
-    dest x as (x1, x2) in 
-    dest y as (y1, y2) in 
+    let '(x1, x2) := x in 
+    let '(y1, y2) := y in 
     if x1 == y1 then 
       if x2 == y2 then in_left
       else in_right
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 835294ce32..842d32fdbc 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -98,8 +98,8 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
 Program Instance [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] => 
   prod_eqdec : EqDec (@eq_setoid (prod A B)) :=
   equiv_dec x y := 
-    dest x as (x1, x2) in 
-    dest y as (y1, y2) in 
+    let '(x1, x2) := x in 
+    let '(y1, y2) := y in 
     if x1 == y1 then 
       if x2 == y2 then in_left
       else in_right
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 8396987ff9..d76c281be1 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -164,7 +164,7 @@ let rec uri_of_constr c =
       uri_of_constr b; url_string " in "; uri_of_constr c
   | RCast (_,c, CastConv (_,t)) ->
       uri_of_constr c; url_string ":"; uri_of_constr t
-  | RRec _ | RIf _ | RLetTuple _ | RLetPattern _ | RCases _ ->
+  | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
       error "Whelp does not support pattern-matching and (co-)fixpoint"
   | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) ->
       anomaly "Written w/o parenthesis"