Integrate a few improvements on typeclasses and Program from the equations branch

and remove equations stuff which moves to a separate plugin.

Classes:
- Ability to define classes post-hoc from constants or inductive types.
- Correctly rebuild the hint database associated to local hypotheses when 
  they are changed by a [Hint Extern] in typeclass resolution.

Tactics and proofs:
- Change [revert] so that it keeps let-ins (but not [generalize]).
- Various improvements to the [generalize_eqs] tactic to make it more robust
  and produce the smallest proof terms possible.
  Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with 
  [generalize_eqs].
- A few new general purpose tactics in Program.Tactics like [revert_until]
- Make transitive closure well-foundedness proofs transparent.
- More uniform testing for metas/evars in pretyping/unification.ml
  (might introduce a few changes in the contribs).

Program:
- Better sorting of dependencies in obligations.
- Ability to start a Program definition from just a type and no obligations, 
  automatically adding an obligation for this type.
- In compilation of Program's well-founded definitions, make the functional a
  separate definition for easier reasoning.
- Add a hint database for every Program populated by [Hint Unfold]s for 
  every defined obligation constant.


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

5 files changed, 141 insertions, 232 deletions

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 0c77a1325..76dc09b26 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -1,4 +1,3 @@
-(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -16,13 +15,31 @@ Require Export JMeq.
 
 Require Import Coq.Program.Tactics.
 
+Ltac is_ground_goal := 
+  match goal with
+    |- ?T => is_ground T
+  end.
+
+(** Try to find a contradiction. *)
+
+Hint Extern 10 => is_ground_goal ; progress (elimtype False).
+
+(** We will use the [block] definition to separate the goal from the 
+   equalities generated by the tactic. *)
+
+Definition block {A : Type} (a : A) := a.
+
+Ltac block_goal := match goal with [ |- ?T ] => change (block T) end.
+Ltac unblock_goal := unfold block in *.
+
 (** Notation for heterogenous equality. *)
 
-Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level).
+Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
 
-(** Notation for the single element of [x = x] *)
+(** Notation for the single element of [x = x] and [x ~= x]. *)
 
-Notation "'refl'" := (@refl_equal _ _).
+Implicit Arguments eq_refl [[A] [x]].
+Implicit Arguments JMeq_refl [[A] [x]].
 
 (** Do something on an heterogeneous equality appearing in the context. *)
 
@@ -77,7 +94,7 @@ Ltac elim_eq_rect :=
       end
   end.
 
-(** Rewrite using uniqueness of indentity proofs [H = refl_equal X]. *)
+(** Rewrite using uniqueness of indentity proofs [H = eq_refl]. *)
 
 Ltac simpl_uip :=
   match goal with
@@ -152,8 +169,21 @@ Ltac clear_eq_proofs :=
 
 Hint Rewrite <- eq_rect_eq : refl_id.
 
-(** The refl_id database should be populated with lemmas of the form
-   [coerce_* t (refl_equal _) = t]. *)
+(** The [refl_id] database should be populated with lemmas of the form
+   [coerce_* t eq_refl = t]. *)
+
+Lemma JMeq_eq_refl {A} (x : A) : JMeq_eq (@JMeq_refl _ x) = eq_refl.
+Proof. intros. apply proof_irrelevance. Qed.
+
+Lemma UIP_refl_refl : Π A (x : A),
+  Eqdep.EqdepTheory.UIP_refl A x eq_refl = eq_refl.
+Proof. intros. apply UIP_refl. Qed.
+
+Lemma inj_pairT2_refl : Π A (x : A) (P : A -> Type) (p : P x),
+  Eqdep.EqdepTheory.inj_pairT2 A P x p p eq_refl = eq_refl.
+Proof. intros. apply UIP_refl. Qed.
+
+Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id.
 
 Ltac rewrite_refl_id := autorewrite with refl_id.
 
@@ -189,45 +219,12 @@ Ltac simplify_eqs :=
 (** A tactic that tries to remove trivial equality guards in induction hypotheses coming
    from [dependent induction]/[generalize_eqs] invocations. *)
 
-Ltac simpl_IH_eq H :=
-  match type of H with
-    | @JMeq _ ?x _ _ -> _ =>
-      refine_hyp (H (JMeq_refl x))
-    | _ -> @JMeq _ ?x _ _ -> _ =>
-      refine_hyp (H _ (JMeq_refl x))
-    | _ -> _ -> @JMeq _ ?x _ _ -> _ =>
-      refine_hyp (H _ _ (JMeq_refl x))
-    | _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ =>
-      refine_hyp (H _ _ _ (JMeq_refl x))
-    | _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ =>
-      refine_hyp (H _ _ _ _ (JMeq_refl x))
-    | _ -> _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ =>
-      refine_hyp (H _ _ _ _ _ (JMeq_refl x))
-    | ?x = _ -> _ =>
-      refine_hyp (H (refl_equal x))
-    | _ -> ?x = _ -> _ =>
-      refine_hyp (H _ (refl_equal x))
-    | _ -> _ -> ?x = _ -> _ =>
-      refine_hyp (H _ _ (refl_equal x))
-    | _ -> _ -> _ -> ?x = _ -> _ =>
-      refine_hyp (H _ _ _ (refl_equal x))
-    | _ -> _ -> _ -> _ -> ?x = _ -> _ =>
-      refine_hyp (H _ _ _ _ (refl_equal x))
-    | _ -> _ -> _ -> _ -> _ -> ?x = _ -> _ =>
-      refine_hyp (H _ _ _ _ _ (refl_equal x))
-  end.
-
-Ltac simpl_IH_eqs H := repeat simpl_IH_eq H.
-
-Ltac do_simpl_IHs_eqs :=
+Ltac simplify_IH_hyps := repeat
   match goal with
-    | [ H : context [ @JMeq _ _ _ _ -> _ ] |- _ ] => progress (simpl_IH_eqs H)
-    | [ H : context [ _ = _ -> _ ] |- _ ] => progress (simpl_IH_eqs H)
+    | [ hyp : _ |- _ ] => specialize_hypothesis hyp
   end.
 
-Ltac simpl_IHs_eqs := repeat do_simpl_IHs_eqs.
-
-(** We split substitution tactics in the two directions depending on which
+(** We split substitution tactics in the two directions depending on which 
    names we want to keep corresponding to the generalization performed by the
    [generalize_eqs] tactic. *)
 
@@ -250,33 +247,16 @@ Ltac inject_right H :=
 Ltac autoinjections_left := repeat autoinjection ltac:inject_left.
 Ltac autoinjections_right := repeat autoinjection ltac:inject_right.
 
-Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ;
-  simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
-
-Ltac simpl_depind_l := subst_left_no_fail ; autoinjections_left ; try discriminates ;
-  simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
+Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ; 
+  simpl_JMeq ; simpl_existTs ; simplify_IH_hyps.
 
-Ltac simpl_depind_r := subst_right_no_fail ; autoinjections_right ; try discriminates ;
-  simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
+Ltac simpl_depind_l := subst_left_no_fail ; autoinjections_left ; try discriminates ; 
+  simpl_JMeq ; simpl_existTs ; simplify_IH_hyps.
 
-(** Support for the [Equations] command.
-   These tactics implement the necessary machinery to solve goals produced by the
-   [Equations] command relative to dependent pattern-matching.
-   It is completely inspired from the "Eliminating Dependent Pattern-Matching" paper by
-   Goguen, McBride and McKinna. *)
+Ltac simpl_depind_r := subst_right_no_fail ; autoinjections_right ; try discriminates ; 
+  simpl_JMeq ; simpl_existTs ; simplify_IH_hyps.
 
-
-(** The NoConfusionPackage class provides a method for making progress on proving a property
-   [P] implied by an equality on an inductive type [I]. The type of [noConfusion] for a given
-   [P] should be of the form [ Π Δ, (x y : I Δ) (x = y) -> NoConfusion P x y ], where
-   [NoConfusion P x y] for constructor-headed [x] and [y] will give a formula ending in [P].
-   This gives a general method for simplifying by discrimination or injectivity of constructors.
-
-   Some actual instances are defined later in the file using the more primitive [discriminate] and
-   [injection] tactics on which we can always fall back.
-   *)
-
-Class NoConfusionPackage (I : Type) := { NoConfusion : Π P : Prop, Type ; noConfusion : Π P, NoConfusion P }.
+Ltac blocked t := block_goal ; t ; unblock_goal.
 
 (** The [DependentEliminationPackage] provides the default dependent elimination principle to
    be used by the [equations] resolver. It is especially useful to register the dependent elimination
@@ -299,18 +279,6 @@ Ltac elim_tac tac p :=
 Ltac elim_case p := elim_tac ltac:(fun p el => destruct p using el) p.
 Ltac elim_ind p := elim_tac ltac:(fun p el => induction p using el) p.
 
-(** The [BelowPackage] class provides the definition of a [Below] predicate for some datatype,
-   allowing to talk about course-of-value recursion on it. *)
-
-Class BelowPackage (A : Type) := {
-  Below : A -> Type ;
-  below : Π (a : A), Below a }.
-
-(** The [Recursor] class defines a recursor on a type, based on some definition of [Below]. *)
-
-Class Recursor (A : Type) (BP : BelowPackage A) :=
-  { rec_type : A -> Type ; rec : Π (a : A), rec_type a }.
-
 (** Lemmas used by the simplifier, mainly rephrasings of [eq_rect], [eq_ind]. *)
 
 Lemma solution_left : Π A (B : A -> Type) (t : A), B t -> (Π x, x = t -> B x).
@@ -332,25 +300,16 @@ Proof. intros. apply X. apply inj_pair2. exact H. Defined.
 Lemma simplification_existT1 : Π A (P : A -> Type) B (p q : A) (x : P p) (y : P q),
   (p = q -> existT P p x = existT P q y -> B) -> (existT P p x = existT P q y -> B).
 Proof. intros. injection H. intros ; auto. Defined.
-
-Lemma simplification_K : Π A (x : A) (B : x = x -> Type), B (refl_equal x) -> (Π p : x = x, B p).
+  
+Lemma simplification_K : Π A (x : A) (B : x = x -> Type), B eq_refl -> (Π p : x = x, B p).
 Proof. intros. rewrite (UIP_refl A). assumption. Defined.
 
-(** Simply unfold as much as possible. *)
-
-Ltac unfold_equations :=
-  unfold solution_left, solution_right, deletion, simplification_heq,
-    simplification_existT1, simplification_existT2, eq_rect_r, eq_rec, eq_ind.
-
-(** The tactic [simplify_equations] is to be used when a program generated using [Equations]
-   is in the goal. It simplifies it as much as possible, possibly using [K] if needed. *)
+(** This hint database and the following tactic can be used with [autounfold] to 
+   unfold everything to [eq_rect]s. *)
 
-Ltac simplify_equations := repeat (unfold_equations ; simplify_eqs).
-
-(** We will use the [block_induction] definition to separate the goal from the
-   equalities generated by the tactic. *)
-
-Definition block_dep_elim {A : Type} (a : A) := a.
+Hint Unfold solution_left solution_right deletion simplification_heq
+  simplification_existT1 simplification_existT2 simplification_K
+  eq_rect_r eq_rec eq_ind : dep_elim.
 
 (** Using these we can make a simplifier that will perform the unification
    steps needed to put the goal in normalised form (provided there are only
@@ -366,19 +325,18 @@ Ltac simplify_one_dep_elim_term c :=
         refine (simplification_existT1 _ _ _ _ _ _ _ _)
     | ?x = ?y -> _ => (* variables case *)
       (let hyp := fresh in intros hyp ;
-        move hyp before x ;
-          generalize dependent x ; refine (solution_left _ _ _ _) ; intros until 0) ||
+        move hyp before x ; revert_until hyp ; generalize dependent x ;
+          refine (solution_left _ _ _ _)(*  ; intros until 0 *)) ||
       (let hyp := fresh in intros hyp ;
-        move hyp before y ;
-          generalize dependent y ; refine (solution_right _ _ _ _) ; intros until 0)
-    | @eq ?A ?t ?u -> ?P => apply (noConfusion (I:=A) P)
+        move hyp before y ; revert_until hyp ; generalize dependent y ;
+          refine (solution_right _ _ _ _)(*  ; intros until 0 *))
     | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H)
     | ?t = ?u -> _ => let hyp := fresh in
       intros hyp ; exfalso ; discriminate
     | ?x = ?y -> _ => let hyp := fresh in
       intros hyp ; (try (clear hyp ; (* If non dependent, don't clear it! *) fail 1)) ;
         case hyp ; clear hyp
-    | block_dep_elim ?T => fail 1 (* Do not put any part of the rhs in the hyps *)
+    | block ?T => fail 1 (* Do not put any part of the rhs in the hyps *)
     | forall x, _ => intro x || (let H := fresh x in rename x into H ; intro x) (* Try to keep original names *)
     | _ => intro
   end.
@@ -393,161 +351,91 @@ Ltac simplify_one_dep_elim :=
 
 Ltac simplify_dep_elim := repeat simplify_one_dep_elim.
 
-(** To dependent elimination on some hyp. *)
-
-Ltac depelim id :=
-  generalize_eqs id ; destruct id ; simplify_dep_elim.
-
 (** Do dependent elimination of the last hypothesis, but not simplifying yet
    (used internally). *)
 
 Ltac destruct_last :=
   on_last_hyp ltac:(fun id => simpl in id ; generalize_eqs id ; destruct id).
 
-(** The rest is support tactics for the [Equations] command. *)
-
-(** Notation for inaccessible patterns. *)
-
-Definition inaccessible_pattern {A : Type} (t : A) := t.
-
-Notation "?( t )" := (inaccessible_pattern t).
-
-(** To handle sections, we need to separate the context in two parts:
-   variables introduced by the section and the rest. We introduce a dummy variable
-   between them to indicate that. *)
-
-CoInductive end_of_section := the_end_of_the_section.
-
-Ltac set_eos := let eos := fresh "eos" in
-  assert (eos:=the_end_of_the_section).
-
-(** We have a specialized [reverse_local] tactic to reverse the goal until the begining of the
-   section variables *)
-
-Ltac reverse_local :=
-  match goal with
-    | [ H : ?T |- _ ] =>
-      match T with
-        | end_of_section => idtac | _ => revert H ; reverse_local end
-    | _ => idtac
-  end.
-
-(** Do as much as possible to apply a method, trying to get the arguments right.
-   !!Unsafe!! We use [auto] for the [_nocomp] variant of [Equations], in which case some
-   non-dependent arguments of the method can remain after [apply]. *)
-
-Ltac simpl_intros m := ((apply m || refine m) ; auto) || (intro ; simpl_intros m).
-
-(** Hopefully the first branch suffices. *)
-
-Ltac try_intros m :=
-  solve [ intros ; unfold block_dep_elim ; refine m || apply m ] ||
-  solve [ unfold block_dep_elim ; simpl_intros m ].
-
-(** To solve a goal by inversion on a particular target. *)
-
-Ltac solve_empty target :=
-  do_nat target intro ; exfalso ; destruct_last ; simplify_dep_elim.
-
-Ltac simplify_method tac := repeat (tac || simplify_one_dep_elim) ; reverse_local.
+Ltac introduce p := first [
+  match p with _ => (* Already there, generalize dependent hyps *)
+    generalize dependent p ; intros p
+  end
+  | intros until p | intros until 1 | intros ].
 
-(** Solving a method call: we can solve it by splitting on an empty family member
-   or we must refine the goal until the body can be applied. *)
+Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)).
+Ltac do_ind p := introduce p ; (induction p || elim_ind p).
 
-Ltac solve_method rec :=
-  match goal with
-    | [ H := ?body : nat |- _ ] => subst H ; clear ; abstract (simplify_method idtac ; solve_empty body)
-    | [ H := [ ?body ] : ?T |- _ ] => clear H ; simplify_method ltac:(exact body) ; rec ; try_intros (body:T)
-  end.
+(** The following tactics allow to do induction on an already instantiated inductive predicate
+   by first generalizing it and adding the proper equalities to the context, in a maner similar to
+   the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
 
-(** Impossible cases, by splitting on a given target. *)
+(** The [do_depelim] higher-order tactic takes an elimination tactic as argument and an hypothesis 
+   and starts a dependent elimination using this tactic. *)
 
-Ltac solve_split :=
+Ltac is_introduced H :=
   match goal with
-    | [ |- let split := ?x : nat in _ ] => clear ; abstract (intros _ ; solve_empty x)
+    | [ H' : _ |- _ ] => match H' with H => idtac end
   end.
 
-(** If defining recursive functions, the prototypes come first. *)
+Tactic Notation "intro_block" hyp(H) :=
+  (is_introduced H ; block_goal ; revert_until H) ||
+    (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal).
 
-Ltac intro_prototypes :=
-  match goal with
-    | [ |- Π x : _, _ ] => intro ; intro_prototypes
-    | _ => idtac
-  end.
+Tactic Notation "intro_block_id" ident(H) :=
+  (is_introduced H ; block_goal ; revert_until H) ||
+    (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal).
 
-Ltac introduce p := first [
-  match p with _ => (* Already there, generalize dependent hyps *)
-    generalize dependent p ; intros p
-  end
-  | intros until p | intros ].
+Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_goal.
 
-Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)).
-Ltac do_ind p := introduce p ; (induction p || elim_ind p).
+Ltac do_intros H :=
+  (try intros until H) ; (intro_block_id H || intro_block H).
 
-Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end.
+Ltac do_depelim_nosimpl tac H := do_intros H ; generalize_eqs H ; tac H.
 
-Ltac un_dep_elimify := unfold block_dep_elim in *.
+Ltac do_depelim tac H := do_depelim_nosimpl tac H ; simpl_dep_elim.
 
-Ltac case_last := dep_elimify ;
-  on_last_hyp ltac:(fun p =>
-    let ty := type of p in
-      match ty with
-        | ?x = ?x => revert p ; refine (simplification_K _ x _ _)
-        | ?x = ?y => revert p
-        | _ => simpl in p ; generalize_eqs p ; do_case p
-      end).
+Ltac do_depind tac H := 
+  (try intros until H) ; intro_block H ;
+  generalize_eqs_vars H ; tac H ; simplify_dep_elim ; simplify_IH_hyps ; unblock_goal.
 
-Ltac nonrec_equations :=
-  solve [solve_equations (case_last) (solve_method idtac)] || solve [ solve_split ]
-    || fail "Unnexpected equations goal".
+(** To dependent elimination on some hyp. *)
 
-Ltac recursive_equations :=
-  solve [solve_equations (case_last) (solve_method ltac:intro)] || solve [ solve_split ]
-    || fail "Unnexpected recursive equations goal".
+Ltac depelim id := do_depelim ltac:(fun hyp => do_case hyp) id.
 
-(** The [equations] tactic is the toplevel tactic for solving goals generated
-   by [Equations]. *)
+(** Used internally. *)
 
-Ltac equations := set_eos ;
-  match goal with
-    | [ |- Π x : _, _ ] => intro ; recursive_equations
-    | _ => nonrec_equations
-  end.
-
-(** The following tactics allow to do induction on an already instantiated inductive predicate
-   by first generalizing it and adding the proper equalities to the context, in a maner similar to
-   the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
+Ltac depelim_nosimpl id := do_depelim_nosimpl ltac:(fun hyp => do_case hyp) id.
 
-(** The [do_depind] higher-order tactic takes an induction tactic as argument and an hypothesis
-   and starts a dependent induction using this tactic. *)
+(** To dependent induction on some hyp. *)
 
-Ltac do_depind tac H :=
-  (try intros until H) ; dep_elimify ; generalize_eqs_vars H ; tac H ; simplify_dep_elim ; un_dep_elimify.
+Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id.
 
 (** A variant where generalized variables should be given by the user. *)
 
-Ltac do_depind' tac H :=
-  (try intros until H) ; dep_elimify ; generalize_eqs H ; tac H ; simplify_dep_elim ; un_dep_elimify.
+Ltac do_depelim' tac H :=
+  (try intros until H) ; block_goal ; generalize_eqs H ; tac H ; simplify_dep_elim ; 
+    simplify_IH_hyps ; unblock_goal.
 
 (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
    By default, we don't try to generalize the hyp by its variable indices.  *)
 
-Tactic Notation "dependent" "destruction" ident(H) :=
-  do_depind' ltac:(fun hyp => do_case hyp) H.
+Tactic Notation "dependent" "destruction" ident(H) := 
+  do_depelim' ltac:(fun hyp => do_case hyp) H.
 
-Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) :=
-  do_depind' ltac:(fun hyp => destruct hyp using c) H.
+Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
+  do_depelim' ltac:(fun hyp => destruct hyp using c) H.
 
-(** This tactic also generalizes the goal by the given variables before the induction. *)
+(** This tactic also generalizes the goal by the given variables before the elimination. *)
 
-Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) :=
-  do_depind' ltac:(fun hyp => revert l ; do_case hyp) H.
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := 
+  do_depelim' ltac:(fun hyp => revert l ; do_case hyp) H.
 
-Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) :=
-  do_depind' ltac:(fun hyp => revert l ; destruct hyp using c) H.
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
+  do_depelim' ltac:(fun hyp => revert l ; destruct hyp using c) H.
 
-(** Then we have wrappers for usual calls to induction. One can customize the induction tactic by
-   writting another wrapper calling do_depind. We suppose the hyp has to be generalized before
+(** Then we have wrappers for usual calls to induction. One can customize the induction tactic by 
+   writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before
    calling [induction]. *)
 
 Tactic Notation "dependent" "induction" ident(H) :=
@@ -558,13 +446,8 @@ Tactic Notation "dependent" "induction" ident(H) "using" constr(c) :=
 
 (** This tactic also generalizes the goal by the given variables before the induction. *)
 
-Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) :=
-  do_depind' ltac:(fun hyp => generalize l ; clear l ; do_ind hyp) H.
-
-Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) :=
-  do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c) H.
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
+  do_depelim' ltac:(fun hyp => generalize l ; clear l ; do_ind hyp) H.
 
-Ltac simplify_IH_hyps := repeat
-  match goal with
-    | [ hyp : _ |- _ ] => specialize_hypothesis hyp
-  end.
\ No newline at end of file
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
+  do_depelim' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c) H.
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index a6aa4d524..89f477d8f 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -82,7 +82,7 @@ Qed.
    in tactics. *)
 
 Definition match_eq (A B : Type) (x : A) (fn : forall (y : A | y = x), B) : B :=
-  fn (exist _ x (refl_equal x)).
+  fn (exist _ x eq_refl).
 
 (* This is what we want to be able to do: replace the originaly matched object by a new,
    propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *)
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index aff2da946..2064977fe 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -46,6 +46,13 @@ Notation " [ ] " := nil : list_scope.
 Notation " [ x ] " := (cons x nil) : list_scope.
 Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
 
+(** Implicit arguments for vectors. *)
+
+Require Import Bvector.
+
+Implicit Arguments Vnil [[A]].
+Implicit Arguments Vcons [[A] [n]].
+
 (** Treating n-ary exists *)
 
 Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p))))
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 881297955..b3b08e067 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -43,7 +43,7 @@ Ltac do_nat n tac :=
 (** Do something on the last hypothesis, or fail *)
 
 Ltac on_last_hyp tac :=
-  match goal with [ H : _ |- _ ] => tac H || fail 1 end.
+  match goal with [ H : _ |- _ ] => first [ tac H | fail 1 ] end.
 
 (** Destructs one pair, without care regarding naming. *)
 
@@ -105,6 +105,15 @@ Ltac revert_last :=
 
 Ltac reverse := repeat revert_last.
 
+(** Reverse everything up to hypothesis id (not included). *)
+
+Ltac revert_until id :=
+  on_last_hyp ltac:(fun id' =>
+    match id' with
+      | id => idtac
+      | _ => revert id' ; revert_until id
+    end).
+
 (** Clear duplicated hypotheses *)
 
 Ltac clear_dup :=
@@ -121,6 +130,16 @@ Ltac clear_dup :=
 
 Ltac clear_dups := repeat clear_dup.
 
+(** Try to clear everything except some hyp *)
+
+Ltac clear_except hyp := 
+  repeat match goal with [ H : _ |- _ ] =>
+           match H with
+             | hyp => fail 1
+             | _ => clear H
+           end
+         end.
+
 (** A non-failing subst that substitutes as much as possible. *)
 
 Ltac subst_no_fail :=
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index bce32af48..c999b58ee 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -29,7 +29,7 @@ Section Wf_Transitive_Closure.
     intros y H2.
     induction H2; auto with sets.
     apply Acc_inv with y; auto with sets.
-  Qed.
+  Defined.
 
   Hint Resolve Acc_clos_trans.
 
@@ -42,6 +42,6 @@ Section Wf_Transitive_Closure.
   Theorem wf_clos_trans : well_founded R -> well_founded trans_clos.
   Proof.
     unfold well_founded in |- *; auto with sets.
-  Qed.
+  Defined.
 
 End Wf_Transitive_Closure.