Add new LetPattern construct to replace dest. syntax: let| pat := t in b is backwards compatible. Update CHANGES with things i've done.

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

20 files changed, 147 insertions, 24 deletions

diff --git a/CHANGES b/CHANGES
index c0fe42112e..17eea233ac 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,6 +7,10 @@ Language
   all arguments are tried successively (from left to right) until one is 
   found that satisfies the structural decreasing condition.
 - Improved inference of implicit arguments.
+- New experimental typeclass system giving ad-hoc polymorphism and overloading based on 
+  dependent records and implicit arguments.
+- New syntax "let| pat := b in c" for binding using irrefutable patterns.
+- New syntax "forall `A`, T" for specifying maximally inserted implicit arguments in terms.
 
 Commands
 
@@ -16,6 +20,8 @@ Commands
   generation of elimination schemes.
 - Modification of the Scheme command so you can ask for the name to be
   automatically computed (e.g. Scheme Induction for nat Sort Set).
+- New command "Combined Scheme" to build combined mutual induction
+  principles from existing mutual induction principles.
 - Source of universe inconsistencies now printed when option 
   "Set Printing Universes" is activated,
 - Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the "compute" 
@@ -63,8 +69,9 @@ Notations and implicit arguments
 - New options "Set Maximal Implicit Insertion", "Set Reversible Pattern
   Implicit", "Set Strongly Strict Implicit" and "Set Printing Implicit
   Defensive" for controlling inference and use of implicit arguments.
-- New modifier in "Implicit Arguments" to force an implicit argument to
-  be maximally inserted.
+- New modifiers in "Implicit Arguments" to force an implicit argument to
+  be maximally inserted and/or forced if it is not seen as inferable.
+- New modifier of "Implicit Arguments" to enrich the set of implicit arguments.
 - Level "constr" moved from 9 to 8.
 - Structure/Record now printed as Record (unless option Printing All is set).
 
@@ -82,6 +89,7 @@ Tactic Language
 - Names to be used as actual identifiers (like f in "apply f_equal f:=t")
   must not be used elsewhere as variables in the same ltac expression
   (possible source of incompatibility).
+- New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression.
 
 Tactics
 
@@ -106,6 +114,31 @@ Tactics
 - New intro pattern "{A,B,C}" synonym to "(A,(B,C))"
 - New syntax "rewrite A,B" for "rewrite A; rewrite B"
 - New syntax "rename a into b, c into d" for "rename a into b; rename c into d"
+- New tactic "dependent induction H [ generalizing id_1 .. id_n ]" to do 
+  induction-inversion on instantiated inductive families à la BasicElim.
+
+Type Classes
+
+- New "Class", "Instance" and "Program Instance" commands to define
+  classes and instances documented in the reference manual.  
+- New binding construct " [ Class_1 param_1 .. param_n, Class_2 ... ] " 
+  for binding type classes usable everywhere.  
+- New command " Print Classes " and " Print Instances some_class " to
+  print tables for typeclasses.  
+- New default eauto hint database "typeclass_instances" used by the default
+  typeclass instance search tactic.  
+- New command " Instanciation Tactic := tac " to customize the typeclass
+  instance search tactic.
+- New theories directory "theories/Classes"
+
+Program
+
+- Moved useful tactics in theories/Program and documented them.
+- More robust obligation handling, dependent pattern-matching and
+  well-founded definitions.
+- New syntax " dest term as pat in term " for destructing objects using
+  an irrefutable pattern while keeping equalities (use this instead of 
+  "let" in Programs).
 
 Miscellaneous
 
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 97f7c1d97a..d3e18371be 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -601,6 +601,9 @@ 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 9bea4f1e02..e6b3ba3ecd 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -689,7 +689,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	build_entry_lc env funnames  avoid b
     | RDynamic _ -> error "Not handled RDynamic"
 and build_entry_lc_from_case env funname make_discr
-    (el:tomatch_tuple)
+    (el:tomatch_tuples)
     (brl:Rawterm.cases_clauses) avoid : 
     rawconstr build_entry_return = 
   match el with 
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index 6632061d49..358c6ba6c7 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -22,7 +22,7 @@ val mkRApp  : rawconstr*(rawconstr list) -> rawconstr
 val mkRLambda : Names.name*rawconstr*rawconstr -> rawconstr
 val mkRProd : Names.name*rawconstr*rawconstr -> rawconstr
 val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr
-val mkRCases : rawconstr option * tomatch_tuple * cases_clauses -> rawconstr
+val mkRCases : rawconstr option * tomatch_tuples * cases_clauses -> rawconstr
 val mkRSort : rawsort -> rawconstr 
 val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *)
 val mkRCast : rawconstr* rawconstr -> rawconstr 
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index a2d5be66c1..0e9e042138 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -488,6 +488,13 @@ 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 j
+
     | RCases (loc,po,tml,eqns) ->
 	Cases.compile_cases loc
 	  ((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 69d5ad67a9..eb69e12257 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -722,6 +722,15 @@ 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,
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b2c7728fdb..156d155667 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -917,6 +917,11 @@ 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 f3c3506b5c..082db5a390 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -64,6 +64,8 @@ let rec unloc = function
         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 97a0f94da5..accccdeee7 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -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 _ | RIf _ | RCast _),_
+    | RPatVar _ | REvar _ | RLetTuple _ | RLetPattern _ | RIf _ | RCast _),_
   | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
-      | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
+      | RPatVar _ | REvar _ | RLetTuple _ | RLetPattern _ | RIf _ | RCast _)
       -> error "Unsupported construction in recursive notations"
   | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _
       -> false
@@ -196,6 +196,7 @@ 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)
@@ -563,6 +564,7 @@ type constr_expr =
       (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
@@ -632,6 +634,7 @@ let constr_loc = function
   | CApp (loc,_,_) -> loc
   | CCases (loc,_,_,_) -> loc
   | CLetTuple (loc,_,_,_,_) -> loc
+  | CLetPattern (loc,_,_,_) -> loc
   | CIf (loc,_,_,_,_) -> loc
   | CHole (loc, _) -> loc
   | CPatVar (loc,_) -> loc
@@ -733,6 +736,10 @@ 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
@@ -844,6 +851,9 @@ let map_constr_expr_with_binders g f e = function
       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 6bbc64cca2..6bfbcf07f8 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -123,6 +123,7 @@ type constr_expr =
       (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/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e55024b516..9972d9e248 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -201,11 +201,15 @@ GEXTEND Gram
 	  ":="; c1 = operconstr LEVEL "200"; "in";
           c2 = operconstr LEVEL "200" ->
           CLetTuple (loc,List.map snd lb,po,c1,c2)
-      | "dest"; c1 = operconstr LEVEL "200"; "as"; p=pattern;
+      | "let"; "|"; p=pattern; ":="; c1 = operconstr LEVEL "200";
           "in"; c2 = operconstr LEVEL "200" ->
-	 let loc' = cases_pattern_expr_loc p in
-         CCases (loc, None, [(c1, (None, None))],
-                 [loc, [loc',[p]], c2])
+	    CLetPattern (loc, p, c1, c2)
+      | "dest"; c1 = operconstr LEVEL "200";
+	  "as"; p=pattern; 
+          "in"; c2 = operconstr LEVEL "200" ->
+	    let loc' = cases_pattern_expr_loc p in
+              CCases (loc, None, [(c1, (None, None))],
+                     [loc, [loc',[p]], c2])
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 8dff6dbf53..7d0d085938 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -36,6 +36,7 @@ let lprod = 200
 let llambda = 200
 let lif = 200
 let lletin = 200
+let lletpattern = 200
 let lfix = 200
 let larrow = 90
 let lcast = 100
@@ -570,6 +571,11 @@ 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/pretyping/cases.ml b/pretyping/cases.ml
index e71083c509..b7317b5be0 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -69,7 +69,7 @@ module type S = sig
     (type_constraint -> env -> rawconstr -> unsafe_judgment) *
       Evd.evar_defs ref ->
     type_constraint -> 
-    env -> rawconstr option * tomatch_tuple * cases_clauses ->
+    env -> rawconstr option * tomatch_tuples * cases_clauses ->
     unsafe_judgment
 end
 
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index adb66ef475..d105ca2d0f 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -53,7 +53,7 @@ module type S = sig
     loc ->
     (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref ->
     type_constraint -> 
-    env -> rawconstr option * tomatch_tuple * cases_clauses ->
+    env -> rawconstr option * tomatch_tuples * cases_clauses ->
     unsafe_judgment
 end
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a9e550bf7c..c9e68d1e3b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -616,7 +616,29 @@ 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
       and b1' = subst_rawconstr subst b1 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c9d44e3dc9..5b4e8e7cf2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -583,6 +583,13 @@ module Pretyping_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 evdref lvar 
+	    (RCases (loc, None, [c], [p]))
+	in j
+	
     | RCases (loc,po,tml,eqns) ->
 	Cases.compile_cases loc
 	  ((fun vtyc env -> pretype vtyc env evdref lvar),evdref)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index bf5cc22723..e7f5de028f 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -62,9 +62,10 @@ 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_tuple * cases_clauses
+  | RCases of loc * 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
@@ -84,10 +85,13 @@ and fix_kind =
 and predicate_pattern =
     name * (loc * inductive * int * name list) option
 
-and tomatch_tuple = (rawconstr * predicate_pattern) list
+and tomatch_tuple = (rawconstr * predicate_pattern)
 
-and cases_clauses =
-    (loc * identifier list * cases_pattern list * rawconstr) list
+and tomatch_tuples = tomatch_tuple list
+
+and cases_clause = (loc * identifier list * cases_pattern list * rawconstr)
+
+and cases_clauses = cases_clause list
 
 let cases_predicate_names tml =
   List.flatten (List.map (function
@@ -117,6 +121,8 @@ let map_rawconstr f = function
         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) ->
@@ -178,6 +184,7 @@ let occur_rawconstr id =
     | 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) ->
@@ -226,6 +233,7 @@ 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 
@@ -277,6 +285,7 @@ let loc_of_rawconstr = function
   | RLambda (loc,_,_,_,_) -> loc
   | RProd (loc,_,_,_,_) -> loc
   | RLetIn (loc,_,_,_) -> loc
+  | RLetPattern (loc,_,_) -> loc
   | RCases (loc,_,_,_) -> loc
   | RLetTuple (loc,_,_,_,_) -> loc
   | RIf (loc,_,_,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 2a5dab6e40..7b342c4115 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -66,9 +66,10 @@ 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_tuple * cases_clauses
+  | RCases of loc * 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
@@ -88,12 +89,15 @@ and fix_kind =
 and predicate_pattern =
     name * (loc * inductive * int * name list) option
 
-and tomatch_tuple = (rawconstr * predicate_pattern) list
+and tomatch_tuple = (rawconstr * predicate_pattern)
 
-and cases_clauses =
-    (loc * identifier list * cases_pattern list * rawconstr) list
+and tomatch_tuples = tomatch_tuple list
 
-val cases_predicate_names : tomatch_tuple -> name list
+and cases_clause = (loc * identifier list * cases_pattern list * rawconstr)
+
+and cases_clauses = cases_clause list
+
+val cases_predicate_names : tomatch_tuples -> name list
 
 (*i - if PRec (_, names, arities, bodies) is in env then arities are
    typed in env too and bodies are typed in env enriched by the
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 7be5141697..65b2968ccd 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -30,7 +30,8 @@ Qed.
 
 Implicit Arguments setoideq_eq [[a] [eqa] [sa]].
 
-Ltac setoideq :=
+(** Application of the extensionality principle for setoids. *)
+Ltac setoideq_ext :=
   match goal with
     [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) X Y)
   end.
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index d76c281be1..8396987ff9 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 _ | RCases _ ->
+  | RRec _ | RIf _ | RLetTuple _ | RLetPattern _ | RCases _ ->
       error "Whelp does not support pattern-matching and (co-)fixpoint"
   | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) ->
       anomaly "Written w/o parenthesis"