Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

56 files changed, 558 insertions, 270 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e53e05d0..faf0482b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: auto.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 09af7f8c..9a0719fc 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: auto.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index c81dcfed..09f80377 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: autorewrite.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Equality
 open Hipattern
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index d6fa2455..b7300cba 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: autorewrite.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Term
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index cf536bfd..73aac029 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: btermdn.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Term
 open Names
@@ -79,8 +79,7 @@ struct
       | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
       | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c])
       | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l)
-      | Sort s when is_small s -> Dn.Label(Term_dn.SortLabel (Some s), [])
-      | Sort _ -> Dn.Label(Term_dn.SortLabel None, [])
+      | Sort _ -> Dn.Label(Term_dn.SortLabel, [])
       | Evar _ -> Dn.Everything
       | _ -> Dn.Nothing
 
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 859890a4..14f9fb23 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: btermdn.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Term
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 7105e84d..afd13b4c 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id$ *)
+(* $Id: class_tactics.ml4 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Pp
 open Util
@@ -69,7 +69,7 @@ let evar_filter evi =
     { evi with 
       evar_hyps = Environ.val_of_named_context hyps';
       evar_filter = List.map (fun _ -> true) hyps' }
-      
+
 let evars_to_goals p evm =
   let goals, evm' =
     Evd.fold
@@ -85,6 +85,7 @@ let evars_to_goals p evm =
     if goals = [] then None
     else
       let goals = List.rev goals in
+      let evm' = evars_reset_evd evm' evm in
 	Some (goals, evm')
 
 (** Typeclasses instance search tactic / eauto *)
@@ -331,7 +332,14 @@ let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
   { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls }
 
 let solve_tac (x : 'a tac) : 'a tac =
-  { skft = fun sk fk gls -> x.skft (fun ({it = gls},_ as res) fk -> if gls = [] then sk res fk else fk ()) fk gls }
+  { skft = fun sk fk gls -> x.skft (fun ({it = gls},_ as res) fk -> 
+    if gls = [] then sk res fk else fk ()) fk gls }
+
+let solve_unif_tac : atac =
+  { skft = fun sk fk {it = gl; sigma = s} -> 
+    try let s' = Evarconv.consider_remaining_unif_problems (Global.env ()) s in
+	  normevars_tac.skft sk fk ({it=gl; sigma=s'})
+    with _ -> fk () }
 
 let hints_tac hints =
   { skft = fun sk fk {it = gl,info; sigma = s} ->
@@ -456,7 +464,6 @@ let then_tac (first : atac) (second : atac) : atac =
 let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option =
   t.skft (fun x _ -> Some x) (fun _ -> None) gl
 
-
 type run_list_res = (auto_result * run_list_res fk) option
 
 let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res =
@@ -491,7 +498,7 @@ let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac =
       let res = run_list_tac tac p goals (make_autogoals ~only_classes ~st goals evm') in
 	match get_result res with
 	| None -> raise Not_found
-	| Some (evm', fk) -> Some (Evd.evars_reset_evd evm' evm, fk)
+	| Some (evm', fk) -> Some (evars_reset_evd evm' evm, fk)
 	    
 let eauto_tac hints = 
   fix (or_tac (then_tac normevars_tac (hints_tac hints)) intro_tac)
@@ -551,16 +558,31 @@ let rec merge_deps deps = function
       else hd :: merge_deps deps tl
 
 let evars_of_evi evi =
-  Intset.union (Evarutil.evars_of_term evi.evar_concl)
-    (match evi.evar_body with
-    | Evar_defined b -> Evarutil.evars_of_term b
-    | Evar_empty -> Intset.empty)
+  Intset.union (evars_of_term evi.evar_concl)
+    (Intset.union
+	(match evi.evar_body with
+	| Evar_empty -> Intset.empty
+	| Evar_defined b -> evars_of_term b)
+	(Evarutil.evars_of_named_context (evar_filtered_context evi)))
+
+let deps_of_constraints cstrs deps =
+  List.fold_right (fun (_, _, x, y) deps -> 
+    let evs = Intset.union (evars_of_term x) (evars_of_term y) in
+      merge_deps evs deps)
+    cstrs deps
+      
+let evar_dependencies evm =
+  Evd.fold 
+    (fun ev evi acc ->
+      merge_deps (Intset.union (Intset.singleton ev) 
+		     (evars_of_evi evi)) acc)
+    evm []
 
 let split_evars evm =
-  Evd.fold (fun ev evi acc ->
-    let deps = Intset.union (Intset.singleton ev) (evars_of_evi evi) in
-      merge_deps deps acc)
-    evm []
+  let _, cstrs = extract_all_conv_pbs evm in
+  let evmdeps = evar_dependencies evm in
+  let deps = deps_of_constraints cstrs evmdeps in
+    List.sort Intset.compare deps
 
 let select_evars evs evm =
   Evd.fold (fun ev evi acc ->
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 44bde497..9ea4892e 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: contradiction.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Term
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 14dcb469..7306f875 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: contradiction.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index eebce493..7866d640 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: decl_interp.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Util
 open Names
diff --git a/tactics/decl_interp.mli b/tactics/decl_interp.mli
index 2d8b2c1d..859db444 100644
--- a/tactics/decl_interp.mli
+++ b/tactics/decl_interp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: decl_interp.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Tacinterp
 open Decl_expr
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 02a0050d..f9a51afe 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: decl_proof_instr.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Pp
diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli
index 170269dc..6f8126ed 100644
--- a/tactics/decl_proof_instr.mli
+++ b/tactics/decl_proof_instr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: decl_proof_instr.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Refiner
 open Names
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 4a779edb..5b7e7e94 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: dhyp.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* Chet's comments about this tactic :
 
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index 5af4e56b..a4be2e42 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: dhyp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index d101b9d7..2b25ad73 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id$ *)
+(* $Id: eauto.ml4 13344 2010-07-28 15:04:36Z msozeau $ *)
 
 open Pp
 open Util
@@ -396,7 +396,7 @@ END
 
 let cons a l = a :: l
 
-let autounfold db cl =
+let autounfolds db occs =
   let unfolds = List.concat (List.map (fun dbname -> 
     let db = try searchtable_map dbname 
       with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
@@ -404,7 +404,15 @@ let autounfold db cl =
     let (ids, csts) = Hint_db.unfolds db in
       Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts
 	(Idset.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db)
-  in unfold_option unfolds cl
+  in unfold_option unfolds
+
+let autounfold db cls gl =
+  let cls = concrete_clause_of cls gl in
+  let tac = autounfolds db in
+  tclMAP (function
+    | OnHyp (id,occs,where) -> tac occs (Some (id,where))
+    | OnConcl occs -> tac occs None)
+    cls gl
 
 let autosimpl db cl =
   let unfold_of_elts constr (b, elts) =
@@ -419,12 +427,13 @@ let autosimpl db cl =
       unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db)
   in unfold_option unfolds cl
 
+open Extraargs
+
 TACTIC EXTEND autounfold
-| [ "autounfold" hintbases(db) "in" hyp(id) ] ->
-    [ autounfold (match db with None -> ["core"] | Some x -> x) (Some (id, InHyp)) ]
-| [ "autounfold" hintbases(db) ] ->
-    [ autounfold (match db with None -> ["core"] | Some x -> x) None ]
-      END
+| [ "autounfold" hintbases(db) in_arg_hyp(id) ] ->
+    [ autounfold (match db with None -> Auto.current_db_names () | Some [] -> ["core"] | Some x -> x) 
+	(glob_in_arg_hyp_to_clause id) ]
+END
 
 let unfold_head env (ids, csts) c = 
   let rec aux c = 
@@ -498,7 +507,7 @@ TACTIC EXTEND autounfoldify
     let db = match kind_of_term x with
       | Const c -> string_of_label (con_label c)
       | _ -> assert false
-    in autounfold ["core";db] None ]
+    in autounfold ["core";db] onConcl ]
 END
 
 TACTIC EXTEND unify
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 331d2b44..eb90b1b6 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -17,6 +17,8 @@ open Environ
 open Explore
 (*i*)
 
+val hintbases : hint_db_name list option Pcoq.Gram.Entry.e
+val wit_hintbases : hint_db_name list option typed_abstract_argument_type
 val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type
 
 val rawwit_auto_using : constr_expr list raw_abstract_argument_type
@@ -36,4 +38,4 @@ val eauto_with_bases :
   bool * int ->
   Term.constr list -> Auto.hint_db list -> Proof_type.tactic
 
-val autounfold : hint_db_name list -> Tacticals.goal_location -> tactic
+val autounfold : hint_db_name list -> Tacticals.clause -> tactic
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 7f1d4249..0372a88d 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: elim.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 8ea6695a..fa18ab0b 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: elim.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 77c878fc..c82e8f64 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: elimschemes.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* Created by Hugo Herbelin from contents related to inductive schemes
    initially developed by Christine Paulin (induction schemes), Vincent
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index 795add12..ba0389e5 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: elimschemes.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Ind_tables
 
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 7ed6bf1e..90e4b44c 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -14,7 +14,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id$ *)
+(* $Id: eqdecide.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Names
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 9972c2a5..22c3b47f 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: eqschemes.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* File created by Hugo Herbelin, Nov 2009 *)
 
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index ae3b1578..447fb359 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: eqschemes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* This file builds schemes relative to equality inductive types *)
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 68f0cc7c..6b16adb4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: equality.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 7c09ae09..f14b3867 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: equality.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 78757939..3e2191d1 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: evar_tactics.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Term
 open Util
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index ed4a33ae..78412150 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: evar_tactics.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Tacmach
 open Names
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index bb63f6b9..c9b2a969 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id$ *)
+(* $Id: extraargs.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Pcoq
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 22a0c2da..e53fc604 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: extraargs.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Tacexpr
 open Term
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 7afd0543..e1ac42c2 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id$ *)
+(* $Id: extratactics.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Pcoq
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 50757148..cfbc8f3d 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: extratactics.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Proof_type
 
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 12ecbd9a..220c00d3 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: hiddentac.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Term
 open Proof_type
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 7bd57cdd..1724bf9c 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: hiddentac.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 3dc9403c..dfa596d3 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*)
 
-(* $Id$ *)
+(* $Id: hipattern.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index f486f348..cf4cdd0d 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: hipattern.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 7290b66b..430f7d5f 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: inv.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 033082e9..eb899699 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: inv.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index c102d8ec..76432dd8 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: leminv.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index 26167978..bdea29df 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: nbtermdn.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Util
 open Names
@@ -117,7 +117,7 @@ let constr_val_discr_st (idpred,cpred) t =
     | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
     | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c])
     | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l)
-    | Sort s -> Dn.Label(Term_dn.SortLabel (Some s), [])
+    | Sort _ -> Dn.Label(Term_dn.SortLabel, [])
     | Evar _ -> Dn.Everything
     | _ -> Dn.Nothing
 
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 3b90b12a..36c54bd3 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: nbtermdn.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
 
 (*i*)
 open Term
@@ -24,7 +24,7 @@ sig
       | GRLabel of global_reference
       | ProdLabel 
       | LambdaLabel
-      | SortLabel of sorts option
+      | SortLabel
   end 
     
   type 'na t
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 87769ccb..06a78011 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: refine.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* JCF -- 6 janvier 1998  EXPERIMENTAL *)
 
diff --git a/tactics/refine.mli b/tactics/refine.mli
index e847a749..55b4033b 100644
--- a/tactics/refine.mli
+++ b/tactics/refine.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: refine.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Tacmach
 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 010fd088..9d99ad96 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -135,8 +135,7 @@ let rewrite_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "rewrit
 let arrow_morphism a b =
   if isprop a && isprop b then
     Lazy.force impl
-  else
-    mkApp(Lazy.force arrow, [|a;b|])
+  else Lazy.force arrow
 
 let setoid_refl pars x =
   applistc (Lazy.force setoid_refl_proj) (pars @ [x])
@@ -176,17 +175,18 @@ let new_cstr_evar (goal,cstr) env t =
   let cstr', t = Evarutil.new_evar cstr env t in
     (goal, cstr'), t
 
-let build_signature evars env m (cstrs : 'a option list) (finalcstr : 'a option) (f : 'a -> constr) =
+let build_signature evars env m (cstrs : (types * types option) option list)
+    (finalcstr : (types * types option) option) =
   let new_evar evars env t =
     new_cstr_evar evars env
       (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
   in
   let mk_relty evars env ty obj =
     match obj with
-      | None ->
+      | None | Some (_, None) ->
 	  let relty = mk_relation ty in
 	    new_evar evars env relty
-      | Some x -> evars, f x
+      | Some (x, Some rel) -> evars, rel
   in
   let rec aux env evars ty l =
     let t = Reductionops.whd_betadeltaiota env (fst evars) ty in
@@ -209,12 +209,11 @@ let build_signature evars env m (cstrs : 'a option list) (finalcstr : 'a option)
       | _, obj :: _ -> anomaly "build_signature: not enough products"
       | _, [] ->
 	  (match finalcstr with
-	  | None ->
+	  | None | Some (_, None) ->
 	      let t = Reductionops.nf_betaiota (fst evars) ty in
 	      let evars, rel = mk_relty evars env t None in
 		evars, t, rel, [t, Some rel]
-	  | Some codom -> let (t, rel) = codom in
-			    evars, t, rel, [t, Some rel])
+	  | Some (t, Some rel) -> evars, t, rel, [t, Some rel])
   in aux env evars m cstrs
 
 let proper_proof env evars carrier relation x =
@@ -248,7 +247,7 @@ type hypinfo = {
   l2r : bool;
   c1 : constr;
   c2 : constr;
-  c  : constr option;
+  c  : constr with_bindings option;
   abs : (constr * types) option;
 }
 
@@ -256,25 +255,35 @@ let evd_convertible env evd x y =
   try ignore(Evarconv.the_conv_x env x y evd); true
   with _ -> false
 
-let decompose_applied_relation env sigma c left2right =
+let rec decompose_app_rel env evd t = 
+  match kind_of_term t with
+  | App (f, args) -> 
+      if Array.length args > 1 then 
+	let fargs, args = array_chop (Array.length args - 2) args in
+	  mkApp (f, fargs), args
+      else 
+	let (f', args) = decompose_app_rel env evd args.(0) in
+	let ty = Typing.type_of env evd args.(0) in
+	let f'' = mkLambda (Name (id_of_string "x"), ty,
+	  mkLambda (Name (id_of_string "y"), lift 1 ty,
+	    mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
+	in (f'', args)
+  | _ -> error "The term provided is not an applied relation."
+
+let decompose_applied_relation env sigma (c,l) left2right =
   let ctype = Typing.type_of env sigma c in
   let find_rel ty =
-    let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
-    let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
-    let rec split_last_two = function
-      | [c1;c2] -> [],(c1, c2)
-      | x::y::z ->
-	  let l,res = split_last_two (y::z) in x::l, res
-      | _ -> error "The term provided is not an applied relation." in
-    let others,(c1,c2) = split_last_two args in
+    let eqclause = Clenv.make_clenv_binding_env_apply env sigma None (c,ty) l in
+    let (equiv, args) = decompose_app_rel env sigma (Clenv.clenv_type eqclause) in
+    let c1 = args.(0) and c2 = args.(1) in 
     let ty1, ty2 =
       Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2
     in
       if not (evd_convertible env eqclause.evd ty1 ty2) then None
       else
 	Some { cl=eqclause; prf=(Clenv.clenv_value eqclause);
-	       car=ty1; rel=mkApp (equiv, Array.of_list others);
-	       l2r=left2right; c1=c1; c2=c2; c=Some c; abs=None }
+	       car=ty1; rel = equiv;
+	       l2r=left2right; c1=c1; c2=c2; c=Some (c,l); abs=None }
   in
     match find_rel ctype with
     | Some c -> c
@@ -398,27 +407,53 @@ let rec decomp_pointwise n c =
   if n = 0 then c
   else
     match kind_of_term c with
-      | App (pointwise, [| a; b; relb |]) -> decomp_pointwise (pred n) relb
-      | _ -> raise Not_found
+    | App (f, [| a; b; relb |]) when eq_constr f (Lazy.force pointwise_relation) ->
+	decomp_pointwise (pred n) relb
+    | App (f, [| a; b; arelb |]) when eq_constr f (Lazy.force forall_relation) ->
+	decomp_pointwise (pred n) (Reductionops.beta_applist (arelb, [mkRel 1]))
+    | _ -> raise (Invalid_argument "decomp_pointwise")
+	
+let rec apply_pointwise rel = function
+  | arg :: args ->
+      (match kind_of_term rel with
+      | App (f, [| a; b; relb |]) when eq_constr f (Lazy.force pointwise_relation) ->
+	  apply_pointwise relb args
+      | App (f, [| a; b; arelb |]) when eq_constr f (Lazy.force forall_relation) ->
+	  apply_pointwise (Reductionops.beta_applist (arelb, [arg])) args
+      | _ -> raise (Invalid_argument "apply_pointwise"))
+  | [] -> rel
+
+let pointwise_or_dep_relation n t car rel =
+  if noccurn 1 car then
+    mkApp (Lazy.force pointwise_relation, [| t; lift (-1) car; lift (-1) rel |])
+  else
+    mkApp (Lazy.force forall_relation, 
+	  [| t; mkLambda (n, t, car); mkLambda (n, t, rel) |])
 
-let lift_cstr env sigma evars args cstr =
+let lift_cstr env sigma evars (args : constr list) ty cstr =
   let cstr =
-    let start =
+    let start env car =
       match cstr with
-      | Some codom -> codom
-      | None ->
-	  let car = Evarutil.e_new_evar evars env (new_Type ()) in
-	  let rel = Evarutil.e_new_evar evars env (mk_relation car) in
-	    (car, rel)
+      | None | Some (_, None) ->
+	  Evarutil.e_new_evar evars env (mk_relation car)
+      | Some (ty, Some rel) -> rel
     in
-      Array.fold_right
-	(fun arg (car, rel) ->
-	  let ty = Typing.type_of env sigma arg in
-	  let car' = mkProd (Anonymous, ty, car) in
-	  let rel' = mkApp (Lazy.force pointwise_relation, [| ty; car; rel |]) in
-	    (car', rel'))
-	args start
-  in Some cstr
+    let rec aux env prod n = 
+      if n = 0 then start env prod
+      else
+	match kind_of_term (Reduction.whd_betadeltaiota env prod) with
+	| Prod (na, ty, b) ->
+	    if noccurn 1 b then
+	      let b' = lift (-1) b in
+	      let rb = aux env b' (pred n) in
+		mkApp (Lazy.force pointwise_relation, [| ty; b'; rb |])
+	    else
+	      let rb = aux (Environ.push_rel (na, None, ty) env) b (pred n) in
+		mkApp (Lazy.force forall_relation, 
+		      [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |])
+	| _ -> assert false
+    in aux env ty (List.length args)
+  in Some (ty, cstr)
 
 let unlift_cstr env sigma = function
   | None -> None
@@ -430,12 +465,17 @@ let default_flags = { under_lambdas = true; on_morphisms = true; }
 
 type evars = evar_map * evar_map (* goal evars, constraint evars *)
 
+type rewrite_proof = 
+  | RewPrf of constr * constr
+  | RewCast of cast_kind
+
+let get_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None
+
 type rewrite_result_info = {
   rew_car : constr;
-  rew_rel : constr;
   rew_from : constr;
   rew_to : constr;
-  rew_prf : constr;
+  rew_prf : rewrite_proof;
   rew_evars : evars;
 }
 
@@ -444,7 +484,13 @@ type rewrite_result = rewrite_result_info option
 type strategy = Environ.env -> evar_map -> constr -> types ->
   constr option -> evars -> rewrite_result option
 
-let resolve_subrelation env sigma car rel rel' res =
+let get_rew_prf r = match r.rew_prf with
+  | RewPrf (rel, prf) -> prf 
+  | RewCast c ->
+      mkCast (mkApp (Coqlib.build_coq_eq_refl (), [| r.rew_car; r.rew_from |]),
+	     c, mkApp (Coqlib.build_coq_eq (), [| r.rew_car; r.rew_from; r.rew_to |]))
+
+let resolve_subrelation env sigma car rel prf rel' res =
   if eq_constr rel rel' then res
   else
 (*   try let evd' = Evarconv.the_conv_x env rel rel' res.rew_evars in *)
@@ -452,12 +498,11 @@ let resolve_subrelation env sigma car rel rel' res =
 (*   with NotConvertible -> *)
     let app = mkApp (Lazy.force subrelation, [|car; rel; rel'|]) in
     let evars, subrel = new_cstr_evar res.rew_evars env app in
+    let appsub = mkApp (subrel, [| res.rew_from ; res.rew_to ; prf |]) in
       { res with
-	rew_prf = mkApp (subrel, [| res.rew_from ; res.rew_to ; res.rew_prf |]);
-	rew_rel = rel';
+	rew_prf = RewPrf (rel', appsub);
 	rew_evars = evars }
 
-
 let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars =
   let evars, morph_instance, proj, sigargs, m', args, args' =
     let first = try (array_find args' (fun i b -> b <> None)) 
@@ -466,9 +511,11 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars
     let morphargs', morphobjs' = array_chop first args' in
     let appm = mkApp(m, morphargs) in
     let appmtype = Typing.type_of env sigma appm in
-    let cstrs = List.map (Option.map (fun r -> r.rew_car, r.rew_rel)) (Array.to_list morphobjs') in
+    let cstrs = List.map (Option.map (fun r -> r.rew_car, get_rew_rel r.rew_prf)) (Array.to_list morphobjs') in
       (* Desired signature *)
-    let evars, appmtype', signature, sigargs = build_signature evars env appmtype cstrs cstr (fun (a,r) -> r) in
+    let evars, appmtype', signature, sigargs = 
+      build_signature evars env appmtype cstrs cstr
+    in
       (* Actual signature found *)
     let cl_args = [| appmtype' ; signature ; appm |] in
     let app = mkApp (Lazy.force proper_type, cl_args) in
@@ -492,7 +539,7 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars
 		  let evars, proof = proper_proof env evars carrier relation x in
 		    [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs'
 	      | Some r ->
-		  [ r.rew_prf; r.rew_to; x ] @ acc, subst, evars, sigargs, r.rew_to :: typeargs')
+		  [ get_rew_prf r; r.rew_to; x ] @ acc, subst, evars, sigargs, r.rew_to :: typeargs')
 	  | None ->
 	      if y <> None then error "Cannot rewrite the argument of a dependent function";
 	      x :: acc, x :: subst, evars, sigargs, x :: typeargs')
@@ -504,10 +551,10 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars
 	[ a, Some r ] -> evars, proof, a, r, oldt, fnewt newt
       | _ -> assert(false)
 
-let apply_constraint env sigma car rel cstr res =
+let apply_constraint env sigma car rel prf cstr res =
   match cstr with
   | None -> res
-  | Some r -> resolve_subrelation env sigma car rel r res
+  | Some r -> resolve_subrelation env sigma car rel prf r res
 
 let eq_env x y = x == y
 
@@ -523,12 +570,14 @@ let apply_rule hypinfo loccs : strategy =
 	match unif with
 	| Some (env', (prf, (car, rel, c1, c2))) when is_occ !occ ->
 	    begin
-	      let goalevars = Evd.evar_merge (fst evars)
-		(Evd.undefined_evars (Evarutil.nf_evar_map env'.evd))
-	      in
-	      let res = { rew_car = ty; rew_rel = rel; rew_from = c1;
-			  rew_to = c2; rew_prf = prf; rew_evars = goalevars, snd evars }
-	      in Some (Some (apply_constraint env sigma car rel cstr res))
+	      if eq_constr t c2 then Some None
+	      else
+		let goalevars = Evd.evar_merge (fst evars)
+		  (Evd.undefined_evars (Evarutil.nf_evar_map env'.evd))
+		in
+		let res = { rew_car = ty; rew_from = c1;
+			    rew_to = c2; rew_prf = RewPrf (rel, prf); rew_evars = goalevars, snd evars }
+		in Some (Some (apply_constraint env sigma car rel prf cstr res))
 	    end
 	| _ -> None
 
@@ -539,24 +588,79 @@ let apply_lemma (evm,c) left2right loccs : strategy =
       apply_rule hypinfo loccs env sigma
 
 let make_leibniz_proof c ty r =
-  let prf = mkApp (Lazy.force coq_f_equal,
-		  [| r.rew_car; ty;
-		     mkLambda (Anonymous, r.rew_car, c (mkRel 1));
-		     r.rew_from; r.rew_to; r.rew_prf |])
+  let prf = 
+    match r.rew_prf with
+    | RewPrf (rel, prf) -> 
+	let rel = mkApp (Lazy.force coq_eq, [| ty |]) in
+	let prf =
+	  mkApp (Lazy.force coq_f_equal,
+		[| r.rew_car; ty;
+		   mkLambda (Anonymous, r.rew_car, c (mkRel 1));
+		   r.rew_from; r.rew_to; prf |])
+	in RewPrf (rel, prf)
+    | RewCast k -> r.rew_prf
   in
-    { r with rew_car = ty; rew_rel = mkApp (Lazy.force coq_eq, [| ty |]);
+    { r with rew_car = ty; 
       rew_from = c r.rew_from; rew_to = c r.rew_to; rew_prf = prf }
 
-let pointwise_or_dep_relation n t car rel =
-  if noccurn 1 car then
-    mkApp (Lazy.force pointwise_relation, [| t; lift (-1) car; lift (-1) rel |])
-  else
-    mkApp (Lazy.force forall_relation, 
-	  [| t; mkLambda (n, t, car); mkLambda (n, t, rel) |])
-
+open Elimschemes
+
+let reset_env env =
+  let env' = Global.env_of_context (Environ.named_context_val env) in
+    Environ.push_rel_context (Environ.rel_context env) env'
+      
+let fold_match ?(force=false) env sigma c =
+  let (ci, p, c, brs) = destCase c in
+  let cty = Retyping.get_type_of env sigma c in
+  let dep, pred, exists, sk = 
+    let env', ctx, body =
+      let ctx, pred = decompose_lam_assum p in
+      let env' = Environ.push_rel_context ctx env in
+	env', ctx, pred
+    in
+    let sortp = Retyping.get_sort_family_of env' sigma body in
+    let sortc = Retyping.get_sort_family_of env sigma cty in
+    let dep = not (noccurn 1 body) in
+    let pred = if dep then p else
+	it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx)
+    in
+    let sk = 
+      if sortp = InProp then
+	if sortc = InProp then
+	  if dep then case_dep_scheme_kind_from_prop
+	  else case_scheme_kind_from_prop
+	else (
+	  if dep
+	  then case_dep_scheme_kind_from_type_in_prop
+	  else case_scheme_kind_from_type)
+      else ((* sortc <> InProp by typing *)
+	if dep
+	then case_dep_scheme_kind_from_type
+	else case_scheme_kind_from_type)
+    in 
+    let exists = Ind_tables.check_scheme sk ci.ci_ind in
+      if exists || force then
+	dep, pred, exists, Ind_tables.find_scheme sk ci.ci_ind
+      else raise Not_found
+  in
+  let app =
+    let ind, args = Inductive.find_rectype env cty in
+    let pars, args = list_chop ci.ci_npar args in
+    let meths = List.map (fun br -> br) (Array.to_list brs) in
+      applist (mkConst sk, pars @ [pred] @ meths @ args @ [c])
+  in 
+    sk, (if exists then env else reset_env env), app
+      
+let unfold_match env sigma sk app =
+  match kind_of_term app with
+  | App (f', args) when f' = mkConst sk ->
+      let v = Environ.constant_value (Global.env ()) sk in
+	Reductionops.whd_beta sigma (mkApp (v, args))
+  | _ -> app
+    
 let subterm all flags (s : strategy) : strategy =
   let rec aux env sigma t ty cstr evars =
-    let cstr' = Option.map (fun c -> (ty, c)) cstr in
+    let cstr' = Option.map (fun c -> (ty, Some c)) cstr in
       match kind_of_term t with
       | App (m, args) ->
 	  let rewrite_args success =
@@ -578,29 +682,39 @@ let subterm all flags (s : strategy) : strategy =
 	      | Some true ->
 		  let args' = Array.of_list (List.rev args') in
 		  let evars', prf, car, rel, c1, c2 = resolve_morphism env sigma t m args args' cstr' evars' in
-		  let res = { rew_car = ty; rew_rel = rel; rew_from = c1;
-			      rew_to = c2; rew_prf = prf; rew_evars = evars' } in
+		  let res = { rew_car = ty; rew_from = c1;
+			      rew_to = c2; rew_prf = RewPrf (rel, prf);
+			      rew_evars = evars' } 
+		  in
 		    Some (Some res)
 	  in
 	    if flags.on_morphisms then
 	      let evarsref = ref (snd evars) in
-	      let cstr' = lift_cstr env sigma evarsref args cstr' in
-	      let m' = s env sigma m (Typing.type_of env sigma m)
-		(Option.map snd cstr') (fst evars, !evarsref)
-	      in
+	      let mty = Typing.type_of env sigma m in
+	      let argsl = Array.to_list args in
+	      let cstr' = lift_cstr env sigma evarsref argsl mty None in
+	      let m' = s env sigma m mty (Option.map snd cstr') (fst evars, !evarsref) in
 		match m' with
 		| None -> rewrite_args None (* Standard path, try rewrite on arguments *)
 		| Some None -> rewrite_args (Some false)
 		| Some (Some r) ->
 		    (* We rewrote the function and get a proof of pointwise rel for the arguments.
 		       We just apply it. *)
-		    let nargs = Array.length args in
+		    let prf = match r.rew_prf with
+		      | RewPrf (rel, prf) ->
+			  RewPrf (apply_pointwise rel argsl, mkApp (prf, args))
+		      | x -> x
+		    in
 		    let res =
-		      { rew_car = decomp_prod env (fst r.rew_evars) nargs r.rew_car;
-			rew_rel = decomp_pointwise nargs r.rew_rel;
+		      { rew_car = prod_appvect r.rew_car args;
 			rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args);
-			rew_prf = mkApp (r.rew_prf, args); rew_evars = r.rew_evars }
-		    in Some (Some res)
+			rew_prf = prf;
+			rew_evars = r.rew_evars }
+		    in 
+		      match prf with
+		      | RewPrf (rel, prf) ->
+			  Some (Some (apply_constraint env sigma res.rew_car rel prf cstr res))
+		      | _ -> Some (Some res)
 	    else rewrite_args None
 
       | Prod (n, x, b) when noccurn 1 b ->
@@ -637,18 +751,24 @@ let subterm all flags (s : strategy) : strategy =
 	  let b' = s env' sigma b (Typing.type_of env' sigma b) (unlift_cstr env sigma cstr) evars in
 	    (match b' with
 	    | Some (Some r) ->
-		Some (Some { r with
-		  rew_prf = mkLambda (n, t, r.rew_prf);
-		  rew_car = mkProd (n, t, r.rew_car);
-		  rew_rel = pointwise_or_dep_relation n t r.rew_car r.rew_rel;
-		  rew_from = mkLambda(n, t, r.rew_from);
-		  rew_to = mkLambda (n, t, r.rew_to) })
+		let prf = match r.rew_prf with
+		  | RewPrf (rel, prf) ->
+		      let rel = pointwise_or_dep_relation n t r.rew_car rel in
+		      let prf = mkLambda (n, t, prf) in
+			RewPrf (rel, prf)
+		  | x -> x
+		in
+		  Some (Some { r with
+		    rew_prf = prf;
+		    rew_car = mkProd (n, t, r.rew_car);
+		    rew_from = mkLambda(n, t, r.rew_from);
+		    rew_to = mkLambda (n, t, r.rew_to) })
 	    | _ -> b')
 
       | Case (ci, p, c, brs) ->
 	  let cty = Typing.type_of env sigma c in
-	  let cstr = Some (mkApp (Lazy.force coq_eq, [| cty |])) in
-	  let c' = s env sigma c cty cstr evars in
+	  let cstr' = Some (mkApp (Lazy.force coq_eq, [| cty |])) in
+	  let c' = s env sigma c cty cstr' evars in
 	    (match c' with
 	    | Some (Some r) ->
 		Some (Some (make_leibniz_proof (fun x -> mkCase (ci, p, x, brs)) ty r))
@@ -668,7 +788,14 @@ let subterm all flags (s : strategy) : strategy =
 			let ctxc x = mkCase (ci, p, c, Array.of_list (List.rev (brs' x))) in
 			  Some (Some (make_leibniz_proof ctxc ty r))
 		    | None -> x
-		else x)
+		else
+		  match try Some (fold_match env sigma t) with Not_found -> None with
+		  | None -> x
+		  | Some (cst, _, t') ->
+		      match aux env sigma t' ty cstr evars with
+		      | Some (Some prf) -> Some (Some { prf with
+			  rew_from = t; rew_to = unfold_match env sigma cst prf.rew_to })
+		      | x' -> x)
 
       | _ -> if all then Some None else None
   in aux
@@ -676,19 +803,27 @@ let subterm all flags (s : strategy) : strategy =
 let all_subterms = subterm true default_flags
 let one_subterm = subterm false default_flags
 
-(** Requires transitivity of the rewrite step, not tail-recursive. *)
+(** Requires transitivity of the rewrite step, if not a reduction.
+    Not tail-recursive. *)
 
 let transitivity env sigma (res : rewrite_result_info) (next : strategy) : rewrite_result option =
-  match next env sigma res.rew_to res.rew_car (Some res.rew_rel) res.rew_evars with
+  match next env sigma res.rew_to res.rew_car (get_rew_rel res.rew_prf) res.rew_evars with
   | None -> None
   | Some None -> Some (Some res)
   | Some (Some res') ->
-      let prfty = mkApp (Lazy.force transitive_type, [| res.rew_car ; res.rew_rel |]) in
-      let evars, prf = new_cstr_evar res'.rew_evars env prfty in
-      let prf = mkApp (prf, [|res.rew_from; res'.rew_from; res'.rew_to;
-			      res.rew_prf; res'.rew_prf |])
-      in Some (Some { res' with rew_from = res.rew_from; rew_evars = evars; rew_prf = prf })
-
+      match res.rew_prf with
+      | RewCast c -> Some (Some { res' with rew_from = res.rew_from })
+      | RewPrf (rew_rel, rew_prf) ->
+	  match res'.rew_prf with
+	  | RewCast _ -> Some (Some ({ res with rew_to = res'.rew_to }))
+	  | RewPrf (res'_rel, res'_prf) ->
+	      let prfty = mkApp (Lazy.force transitive_type, [| res.rew_car; rew_rel |]) in
+	      let evars, prf = new_cstr_evar res'.rew_evars env prfty in
+	      let prf = mkApp (prf, [|res.rew_from; res'.rew_from; res'.rew_to;
+				      rew_prf; res'_prf |])
+	      in Some (Some { res' with rew_from = res.rew_from; 
+		rew_evars = evars; rew_prf = RewPrf (res'_rel, prf) })
+		
 (** Rewriting strategies.
 
     Inspired by ELAN's rewriting strategies:
@@ -714,8 +849,8 @@ module Strategies =
 	  let mty = mkApp (Lazy.force proper_proxy_type, [| ty ; rel; t |]) in
 	    new_cstr_evar evars env mty
 	in
-	  Some (Some { rew_car = ty; rew_rel = rel; rew_from = t; rew_to = t;
-		       rew_prf = proof; rew_evars = evars })
+	  Some (Some { rew_car = ty; rew_from = t; rew_to = t;
+		       rew_prf = RewPrf (rel, proof); rew_evars = evars })
 
     let progress (s : strategy) : strategy =
       fun env sigma t ty cstr evars ->
@@ -769,13 +904,24 @@ module Strategies =
 
     let old_hints (db : string) : strategy =
       let rules = Autorewrite.find_rewrites db in
-	lemmas (List.map (fun hint -> (inj_open hint.Autorewrite.rew_lemma, hint.Autorewrite.rew_l2r)) rules)
+	lemmas (List.map (fun hint -> (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r)) rules)
 
     let hints (db : string) : strategy =
       fun env sigma t ty cstr evars ->
-	let rules = Autorewrite.find_matches db t in
-	  lemmas (List.map (fun hint -> (inj_open hint.Autorewrite.rew_lemma, hint.Autorewrite.rew_l2r)) rules)
-	    env sigma t ty cstr evars
+      let rules = Autorewrite.find_matches db t in
+	lemmas (List.map (fun hint -> (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r)) rules)
+	  env sigma t ty cstr evars
+
+    let reduce (r : Redexpr.red_expr) : strategy =
+      let rfn, ckind = Redexpr.reduction_of_red_expr r in
+	fun env sigma t ty cstr evars ->
+	  let t' = rfn env sigma t in
+	    if eq_constr t' t then
+	      Some None
+	    else
+	      Some (Some { rew_car = ty; rew_from = t; rew_to = t';
+			   rew_prf = RewCast ckind; rew_evars = evars })
+	  
 
 end
 
@@ -787,7 +933,7 @@ let rewrite_strat flags occs hyp =
     Strategies.choice app (subterm true flags (fun env -> aux () env))
   in aux ()
 
-let rewrite_with (evm,c) left2right loccs : strategy =
+let rewrite_with {it = c; sigma = evm} left2right loccs : strategy =
   fun env sigma ->
     let evars = Evd.merge sigma evm in
     let hypinfo = ref (decompose_applied_relation env evars c left2right) in
@@ -803,7 +949,7 @@ let apply_strategy (s : strategy) env sigma concl cstr evars =
     | Some None -> Some None
     | Some (Some res) ->
 	evars := res.rew_evars;
-	Some (Some (res.rew_prf, (res.rew_car, res.rew_rel, res.rew_from, res.rew_to)))
+	Some (Some (res.rew_prf, (res.rew_car, res.rew_from, res.rew_to)))
 
 let split_evars_once sigma evd =
   Evd.fold (fun ev evi deps ->
@@ -834,6 +980,12 @@ let solve_constraints env evars =
 let nf_zeta =
   Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
 
+let map_rewprf f = function
+  | RewPrf (rel, prf) -> RewPrf (f rel, f prf)
+  | RewCast c -> RewCast c
+
+exception RewriteFailure
+
 let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
   let concl, is_hyp =
     match clause with
@@ -852,12 +1004,14 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
   let env = pf_env gl in
   let eq = apply_strategy strat env sigma concl (Some cstr) evars in
     match eq with
-    | Some (Some (p, (_, _, oldt, newt))) ->
+    | Some (Some (p, (car, oldt, newt))) ->
 	(try
 	    let cstrevars = !evars in
 	    let evars = solve_constraints env cstrevars in
-	    let p = Evarutil.nf_evar evars p in
-	    let p = nf_zeta env evars p in
+	    let p = map_rewprf 
+	      (fun p -> nf_zeta env evars (Evarutil.nf_evar evars p)) 
+	      p 
+	    in
 	    let newt = Evarutil.nf_evar evars newt in
 	    let abs = Option.map (fun (x, y) ->
 	      Evarutil.nf_evar evars x, Evarutil.nf_evar evars y) abs in
@@ -865,27 +1019,36 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
 	    let rewtac =
 	      match is_hyp with
 	      | Some id ->
-		  let term =
-		    match abs with
-		    | None -> p
-		    | Some (t, ty) ->
-			mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |])
-		  in
-		    cut_replacing id newt
-		      (Tacmach.refine_no_check (mkApp (term, [| mkVar id |])))
+		  (match p with
+		  | RewPrf (rel, p) ->
+		      let term =
+			match abs with
+			| None -> p
+			| Some (t, ty) ->
+			    mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |])
+		      in
+			cut_replacing id newt
+			  (Tacmach.refine_no_check (mkApp (term, [| mkVar id |])))
+		  | RewCast c ->
+		      change_in_hyp None newt (id, InHypTypeOnly))
+		    
 	      | None ->
-		  (match abs with
-		  | None ->
-		      let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
-			tclTHENLAST
-			  (Tacmach.internal_cut_no_check false name newt)
-			  (tclTHEN (Tactics.revert [name]) (Tacmach.refine_no_check p))
-		  | Some (t, ty) ->
-		      Tacmach.refine_no_check
-			(mkApp (mkLambda (Name (id_of_string "newt"), newt,
-					 mkLambda (Name (id_of_string "lemma"), ty,
-						  mkApp (p, [| mkRel 2 |]))),
-			       [| mkMeta goal_meta; t |])))
+		  (match p with
+		  | RewPrf (rel, p) ->
+		      (match abs with
+		      | None ->
+			  let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
+			    tclTHENLAST
+			      (Tacmach.internal_cut_no_check false name newt)
+			      (tclTHEN (Tactics.revert [name]) (Tacmach.refine_no_check p))
+		      | Some (t, ty) ->
+			  Tacmach.refine_no_check
+			    (mkApp (mkLambda (Name (id_of_string "newt"), newt,
+					     mkLambda (Name (id_of_string "lemma"), ty,
+						      mkApp (p, [| mkRel 2 |]))),
+				   [| mkMeta goal_meta; t |])))
+		  | RewCast c -> 
+		      change_in_concl None newt)
 	    in
 	    let evartac =
 	      if not (undef = Evd.empty) then
@@ -900,14 +1063,14 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
 			++ fnl () ++ Himsg.explain_typeclass_error env e)) gl)
     | Some None ->
 	tclFAIL 0 (str"setoid rewrite failed: no progress made") gl
-    | None -> raise Not_found
+    | None -> raise RewriteFailure
 
 let cl_rewrite_clause_strat strat clause gl =
   init_setoid ();
   let meta = Evarutil.new_meta() in
   let gl = { gl with sigma = Typeclasses.mark_unresolvables gl.sigma } in
     try cl_rewrite_clause_aux strat meta clause gl
-    with Not_found ->
+    with RewriteFailure ->
       tclFAIL 0 (str"setoid rewrite failed: strategy failed") gl
 
 let cl_rewrite_clause l left2right occs clause gl =
@@ -939,11 +1102,13 @@ let glob_strategy ist l = l
 let subst_strategy evm l = l
 
 let apply_constr_expr c l2r occs = fun env sigma ->
-  let c = Constrintern.interp_open_constr sigma env c in
-    apply_lemma c l2r occs env sigma
+  let evd, c = Constrintern.interp_open_constr sigma env c in
+    apply_lemma (evd, (c, NoBindings)) l2r occs env sigma
 
-let interp_constr_list env sigma cs =
-  List.map (fun c -> Constrintern.interp_open_constr sigma env c, true) cs
+let interp_constr_list env sigma =
+  List.map (fun c -> 
+	      let evd, c = Constrintern.interp_open_constr sigma env c in
+		(evd, (c, NoBindings)), true)
 
 open Pcoq
 
@@ -980,15 +1145,18 @@ ARGUMENT EXTEND rewstrategy TYPED AS strategy
   | [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ Strategies.choice h h' ]
   | [ "old_hints" preident(h) ] -> [ Strategies.old_hints h ]
   | [ "hints" preident(h) ] -> [ Strategies.hints h ]
-  | [ "terms" constr_list(h) ] -> [ fun env sigma -> Strategies.lemmas (interp_constr_list env sigma h) env sigma ]
+  | [ "terms" constr_list(h) ] -> [ fun env sigma -> 
+      Strategies.lemmas (interp_constr_list env sigma h) env sigma ]
+  | [ "eval" red_expr(r) ] -> [ fun env sigma -> 
+      Strategies.reduce (Tacinterp.interp_redexp env sigma r) env sigma ]
 END
 
 TACTIC EXTEND class_rewrite
-| [ "clrewrite" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ]
-| [ "clrewrite" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ]
-| [ "clrewrite" orient(o) open_constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o all_occurrences (Some id) ]
-| [ "clrewrite" orient(o) open_constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) None ]
-| [ "clrewrite" orient(o) open_constr(c) ] -> [ cl_rewrite_clause c o all_occurrences None ]
+| [ "clrewrite" orient(o) constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ]
+| [ "clrewrite" orient(o) constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ]
+| [ "clrewrite" orient(o) constr_with_bindings(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o all_occurrences (Some id) ]
+| [ "clrewrite" orient(o) constr_with_bindings(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) None ]
+| [ "clrewrite" orient(o) constr_with_bindings(c) ] -> [ cl_rewrite_clause c o all_occurrences None ]
     END
 
 TACTIC EXTEND class_rewrite_strat
@@ -998,7 +1166,7 @@ END
 
 
 let clsubstitute o c =
-  let is_tac id = match kind_of_term (snd c) with Var id' when id' = id -> true | _ -> false in
+  let is_tac id = match kind_of_term (fst c.it) with Var id' when id' = id -> true | _ -> false in
     Tacticals.onAllHypsAndConcl
       (fun cl ->
 	match cl with
@@ -1006,22 +1174,22 @@ let clsubstitute o c =
 	  | _ -> tclTRY (cl_rewrite_clause c o all_occurrences cl))
 
 TACTIC EXTEND substitute
-| [ "substitute" orient(o) open_constr(c) ] -> [ clsubstitute o c ]
+| [ "substitute" orient(o) constr_with_bindings(c) ] -> [ clsubstitute o c ]
 END
 
 
 (* Compatibility with old Setoids *)
 
 TACTIC EXTEND setoid_rewrite
-   [ "setoid_rewrite" orient(o) open_constr(c) ]
+   [ "setoid_rewrite" orient(o) constr_with_bindings(c) ]
    -> [ cl_rewrite_clause c o all_occurrences None ]
- | [ "setoid_rewrite" orient(o) open_constr(c) "in" hyp(id) ] ->
+ | [ "setoid_rewrite" orient(o) constr_with_bindings(c) "in" hyp(id) ] ->
       [ cl_rewrite_clause c o all_occurrences (Some id)]
- | [ "setoid_rewrite" orient(o) open_constr(c) "at" occurrences(occ) ] ->
+ | [ "setoid_rewrite" orient(o) constr_with_bindings(c) "at" occurrences(occ) ] ->
       [ cl_rewrite_clause c o (occurrences_of occ) None]
- | [ "setoid_rewrite" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id)] ->
+ | [ "setoid_rewrite" orient(o) constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] ->
       [ cl_rewrite_clause c o (occurrences_of occ) (Some id)]
- | [ "setoid_rewrite" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ)] ->
+ | [ "setoid_rewrite" orient(o) constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ)] ->
       [ cl_rewrite_clause c o (occurrences_of occ) (Some id)]
 END
 
@@ -1104,12 +1272,12 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	     (Ident (dummy_loc,id_of_string "Equivalence_Symmetric"), lemma2);
 	     (Ident (dummy_loc,id_of_string "Equivalence_Transitive"), lemma3)])
 
-type 'a binders_let_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
+type 'a binders_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
 
-let (wit_binders_let : Genarg.tlevel binders_let_argtype),
-  (globwit_binders_let : Genarg.glevel binders_let_argtype),
-  (rawwit_binders_let : Genarg.rlevel binders_let_argtype) =
-  Genarg.create_arg "binders_let"
+let (wit_binders : Genarg.tlevel binders_argtype),
+  (globwit_binders : Genarg.glevel binders_argtype),
+  (rawwit_binders : Genarg.rlevel binders_argtype) =
+  Genarg.create_arg "binders"
 
 open Pcoq.Constr
 
@@ -1147,35 +1315,35 @@ VERNAC COMMAND EXTEND AddRelation3
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation
-  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)
+  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
 	"reflexivity" "proved" "by" constr(lemma1)
 	"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None ]
-  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)
+  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
 	"reflexivity" "proved" "by" constr(lemma1)
 	"as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n (Some lemma1) None None ]
-  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
+  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n None None None ]
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation2
-    [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+    [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n None (Some lemma2) None ]
-  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
+  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) ]
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation3
-    [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+    [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) ]
-  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ]
-  | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
 	"as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n None None (Some lemma3) ]
 END
@@ -1242,7 +1410,7 @@ let build_morphism_signature m =
 	| _ -> []
     in aux t
   in
-  let evars, t', sig_, cstrs = build_signature !isevars env t cstrs None snd in
+  let evars, t', sig_, cstrs = build_signature !isevars env t cstrs None in
   let _ = isevars := evars in
   let _ = List.iter
     (fun (ty, rel) ->
@@ -1264,7 +1432,7 @@ let default_morphism sign m =
   let env = Global.env () in
   let t = Typing.type_of env Evd.empty m in
   let evars, _, sign, cstrs =
-    build_signature (Evd.empty,Evd.empty) env t (fst sign) (snd sign) (fun (ty, rel) -> rel)
+    build_signature (Evd.empty,Evd.empty) env t (fst sign) (snd sign)
   in
   let morph =
     mkApp (Lazy.force proper_type, [| t; sign; m |])
@@ -1324,13 +1492,13 @@ let add_morphism glob binders m s n =
 VERNAC COMMAND EXTEND AddSetoid1
    [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      [ add_setoid [] a aeq t n ]
-  | [ "Add" "Parametric" "Setoid" binders_let(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+  | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      [	add_setoid binders a aeq t n ]
   | [ "Add" "Morphism" constr(m) ":" ident(n) ] ->
       [ add_morphism_infer (not (Vernacexpr.use_section_locality ())) m n ]
   | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] ->
       [ add_morphism (not (Vernacexpr.use_section_locality ())) [] m s n ]
-  | [ "Add" "Parametric" "Morphism" binders_let(binders) ":" constr(m)
+  | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
 	"with" "signature" lconstr(s) "as" ident(n) ] ->
       [ add_morphism (not (Vernacexpr.use_section_locality ())) binders m s n ]
 END
@@ -1390,16 +1558,16 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
   let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in
     {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)}
 
-let get_hyp gl evars c clause l2r =
-  let hi = decompose_applied_relation (pf_env gl) evars c l2r in
+let get_hyp gl evars (c,l) clause l2r =
+  let hi = decompose_applied_relation (pf_env gl) evars (c,l) l2r in
   let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in
     unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl
 
-let general_rewrite_flags = { under_lambdas = false; on_morphisms = false }
+let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
 
-let apply_lemma gl c cl l2r occs =
+let apply_lemma gl (c,l) cl l2r occs =
   let sigma = project gl in
-  let hypinfo = ref (get_hyp gl sigma c cl l2r) in
+  let hypinfo = ref (get_hyp gl sigma (c,l) cl l2r) in
   let app = apply_rule hypinfo occs in
   let rec aux () =
     Strategies.choice app (subterm true general_rewrite_flags (fun env -> aux () env))
@@ -1407,12 +1575,12 @@ let apply_lemma gl c cl l2r occs =
 
 let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
   let meta = Evarutil.new_meta() in
-  let hypinfo, strat = apply_lemma gl c cl l2r occs in
+  let hypinfo, strat = apply_lemma gl (c,l) cl l2r occs in
     try
       tclTHEN
         (Refiner.tclEVARS hypinfo.cl.evd)
         (cl_rewrite_clause_aux ~abs:hypinfo.abs strat meta cl) gl
-    with Not_found ->
+    with RewriteFailure ->
       let {l2r=l2r; c1=x; c2=y} = hypinfo in
 	raise (Pretype_errors.PretypeError
 		  (pf_env gl,
@@ -1441,18 +1609,10 @@ let not_declared env ty rel =
   tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++
 		str ty ++ str" relation. Maybe you need to require the Setoid library")
 
-let relation_of_constr env c =
-  match kind_of_term c with
-    | App (f, args) when Array.length args >= 2 ->
-	let relargs, args = array_chop (Array.length args - 2) args in
-	  mkApp (f, relargs), args
-    | _ -> errorlabstrm "relation_of_constr"
-	(str "The term " ++ Printer.pr_constr_env env c ++ str" is not an applied relation.")
-
 let setoid_proof gl ty fn fallback =
   let env = pf_env gl in
     try
-      let rel, args = relation_of_constr env (pf_concl gl) in
+      let rel, args = decompose_app_rel env (project gl) (pf_concl gl) in
       let evm, car = project gl, pf_type_of gl args.(0) in
 	fn env evm car rel gl
     with e ->
@@ -1460,7 +1620,7 @@ let setoid_proof gl ty fn fallback =
       with Hipattern.NoEquationFound ->
 	  match e with
 	  | Not_found ->
-	      let rel, args = relation_of_constr env (pf_concl gl) in
+	      let rel, args = decompose_app_rel env (project gl) (pf_concl gl) in
 		not_declared env ty rel gl
 	  | _ -> raise e
 
@@ -1480,8 +1640,7 @@ let setoid_transitivity c gl =
       let proof = get_transitive_proof env evm car rel in
       match c with
       | None -> eapply proof
-      | Some c ->
-	  apply_with_bindings (proof,Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ]))
+      | Some c -> apply_with_bindings (proof,Rawterm.ImplicitBindings [ c ]))
     (transitivity_red true c)
 
 let setoid_symmetry_in id gl =
@@ -1539,3 +1698,25 @@ let implify id gl =
 TACTIC EXTEND implify
 [ "implify" hyp(n) ] -> [ implify n ]
 END
+
+let rec fold_matches env sigma c =
+  map_constr_with_full_binders Environ.push_rel 
+    (fun env c ->
+      match kind_of_term c with
+      | Case _ ->
+          let cst, env, c' = fold_match ~force:true env sigma c in
+	    fold_matches env sigma c'
+      | _ -> fold_matches env sigma c)
+    env c
+
+TACTIC EXTEND fold_match
+[ "fold_match" constr(c) ] -> [ fun gl -> 
+  let _, _, c' = fold_match ~force:true (pf_env gl) (project gl) c in
+    change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl gl ]
+END
+
+TACTIC EXTEND fold_matches
+| [ "fold_matches" constr(c) ] -> [ fun gl -> 
+  let c' = fold_matches (pf_env gl) (project gl) c in
+    change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl gl ]
+END
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 291df0fe..95e44c40 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: tacinterp.ml 13360 2010-07-30 08:47:08Z herbelin $ *)
 
 open Constrintern
 open Closure
@@ -2415,7 +2415,9 @@ and interp_atomic ist gl tac =
   | TacChange (Some op,c,cl) ->
       let sign,op = interp_typed_pattern ist env sigma op in
       h_change (Some op)
-        (pf_interp_constr ist (extend_gl_hyps gl sign) c)
+        (try pf_interp_constr ist (extend_gl_hyps gl sign) c
+	 with Not_found | Anomaly _ (* Hack *) ->
+	   errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side."))
         (interp_clause ist gl cl)
 
   (* Equivalence relations *)
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 854664e9..82f4d99a 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: tacinterp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml
new file mode 100644
index 00000000..df5a3283
--- /dev/null
+++ b/tactics/tactic_option.ml
@@ -0,0 +1,57 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: subtac.ml 12623 2010-01-04 17:50:38Z letouzey $ *)
+
+open Libobject
+open Proof_type
+open Pp
+
+let declare_tactic_option ?(default=Tacexpr.TacId []) name =
+  let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref default in
+  let default_tactic : Proof_type.tactic ref = ref (Tacinterp.eval_tactic !default_tactic_expr) in
+  let locality = ref false in
+  let set_default_tactic local t = 
+    locality := local;
+    default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t 
+  in
+  let cache (_, (local, tac)) = set_default_tactic local tac in
+  let load (_, (local, tac)) =
+    if not local then set_default_tactic local tac
+  in
+  let subst (s, (local, tac)) =
+    (local, Tacinterp.subst_tactic s tac)
+  in
+  let input, _output = 
+    declare_object
+      { (default_object name) with
+	cache_function = cache;
+	load_function = (fun _ -> load);
+	open_function = (fun _ -> load);
+	classify_function = (fun (local, tac) ->
+	  if local then Dispose else Substitute (local, tac));
+	subst_function = subst}
+  in
+  let put local tac =
+    set_default_tactic local tac;
+    Lib.add_anonymous_leaf (input (local, tac))
+  in
+  let get () = !locality, !default_tactic in
+  let print () = 
+    Pptactic.pr_glob_tactic (Global.env ()) !default_tactic_expr ++
+      (if !locality then str" (locally defined)" else str" (globally defined)")
+  in
+  let freeze () = !locality, !default_tactic_expr in
+  let unfreeze (local, t) = set_default_tactic local t in
+  let init () = () in
+    Summary.declare_summary name
+      { Summary.freeze_function = freeze;
+        Summary.unfreeze_function = unfreeze;
+        Summary.init_function = init };
+    put, get, print
+      
diff --git a/tactics/tactic_option.mli b/tactics/tactic_option.mli
new file mode 100644
index 00000000..890ba98e
--- /dev/null
+++ b/tactics/tactic_option.mli
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: subtac.ml 12623 2010-01-04 17:50:38Z letouzey $ *)
+
+open Proof_type
+open Tacexpr
+open Vernacexpr
+
+val declare_tactic_option : ?default:Tacexpr.glob_tactic_expr -> string -> 
+  (* put *) (locality_flag -> glob_tactic_expr -> unit) *
+  (* get *) (unit -> locality_flag * tactic) *
+  (* print *) (unit -> Pp.std_ppcmds)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 59a8b794..171a35c0 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: tacticals.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 90508436..af74e382 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: tacticals.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e09707ab..9e4be0af 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: tactics.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Pp
 open Util
@@ -2320,6 +2320,9 @@ let linear vars args =
       true
     with Seen -> false
 
+let is_defined_variable env id =
+  pi2 (lookup_named id env) <> None
+
 let abstract_args gl generalize_vars dep id defined f args =
   let sigma = project gl in
   let env = pf_env gl in
@@ -2347,7 +2350,7 @@ let abstract_args gl generalize_vars dep id defined f args =
     let liftargty = lift lenctx argty in
     let leq = constr_cmp Reduction.CUMUL liftargty ty in
       match kind_of_term arg with
-      | Var id when leq && not (Idset.mem id nongenvars) ->
+      | Var id when not (is_defined_variable env id) && leq && not (Idset.mem id nongenvars) ->
       	  (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls,
       	  Idset.add id nongenvars, Idset.remove id vars, env)
       | _ ->
@@ -2374,7 +2377,7 @@ let abstract_args gl generalize_vars dep id defined f args =
     let parvars = ids_of_constr ~all:true Idset.empty f' in
       if not (linear parvars args') then true, f, args
       else
-	match array_find_i (fun i x -> not (isVar x)) args' with
+	match array_find_i (fun i x -> not (isVar x) || is_defined_variable env (destVar x)) args' with
 	| None -> false, f', args'
 	| Some nonvar ->
 	    let before, after = array_chop nonvar args' in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 92477e23..bfc32654 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: tactics.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 0a634138..b885b152 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -21,3 +21,4 @@ Evar_tactics
 Autorewrite
 Decl_interp
 Decl_proof_instr
+Tactic_option
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 6091e3d1..a7e7613d 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(*i $Id$ i*)
+(*i $Id: tauto.ml4 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Term
 open Hipattern
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 828fc065..f9f086d9 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: termdn.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Util
 open Names
@@ -33,7 +33,7 @@ struct
     | GRLabel of global_reference
     | ProdLabel 
     | LambdaLabel
-    | SortLabel of sorts option
+    | SortLabel
 	
   module Y =  struct 
      type t = term_label
@@ -97,12 +97,7 @@ let constr_pat_discr_st (idpred,cpred) t =
       Some (GRLabel ref, args)
   | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c])
   | PLambda (_, d, c), l -> Some (LambdaLabel, [d ; c] @ l)
-  | PSort s, [] -> 
-      let s' = match s with
-	| RProp c -> Some (Prop c)
-	| RType _ -> None 
-	    (* Don't try to be clever about type levels here *)
-      in Some (SortLabel s', [])
+  | PSort s, [] -> Some (SortLabel, [])
   | _ -> None
 
 open Dn
@@ -125,8 +120,7 @@ let constr_val_discr_st (idpred,cpred) t =
     | Var id when not (Idpred.mem id idpred) -> Label(GRLabel (VarRef id),l)
     | Prod (n, d, c) -> Label(ProdLabel, [d; c])
     | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l)
-    | Sort s when is_small s -> Label(SortLabel (Some s), [])
-    | Sort _ -> Label (SortLabel None, [])
+    | Sort _ -> Label (SortLabel, [])
     | Evar _ -> Everything
     | _ -> Nothing
 
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index b7c9f273..e778de8d 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: termdn.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
 
 (*i*)
 open Term
@@ -58,7 +58,7 @@ sig
     | GRLabel of global_reference
     | ProdLabel 
     | LambdaLabel
-    | SortLabel of sorts option
+    | SortLabel
 	
   val constr_pat_discr_st : transparent_state ->
     constr_pattern -> (term_label * constr_pattern list) option