Move Program tactics into a proper theories/ directory as they are general purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module.

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

15 files changed, 197 insertions, 132 deletions

diff --git a/Makefile.common b/Makefile.common
index cd0d6ab790..1325eabcf1 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -751,9 +751,9 @@ CCVO:=
 
 DPVO:=contrib/dp/Dp.vo
 
-SUBTACVO:=contrib/subtac/SubtacTactics.vo contrib/subtac/Heq.vo \
-	contrib/subtac/Utils.vo contrib/subtac/FixSub.vo contrib/subtac/Subtac.vo \
-	contrib/subtac/FunctionalExtensionality.vo
+SUBTACVO:=theories/Program/Tactics.vo theories/Program/Heq.vo \
+	theories/Program/Utils.vo theories/Program/FixSub.vo theories/Program/Program.vo \
+	theories/Program/FunctionalExtensionality.vo
 
 RTAUTOVO:= \
  contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo
diff --git a/contrib/subtac/Heq.v b/contrib/subtac/Heq.v
deleted file mode 100644
index f2b216d960..0000000000
--- a/contrib/subtac/Heq.v
+++ /dev/null
@@ -1,34 +0,0 @@
-Require Export JMeq.
-
-(** 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).
-
-(** Do something on an heterogeneous equality appearing in the context. *)
-
-Ltac on_JMeq tac := 
-  match goal with
-    | [ H : @JMeq ?x ?X ?y ?Y |- _ ] => tac H
-  end.
-
-(** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *)
-
-Ltac simpl_one_JMeq :=
-  on_JMeq 
-  ltac:(fun H => let H' := fresh "H" in 
-    assert (H' := JMeq_eq H) ; clear H ; rename H' into H).
-
-(** Repeat it for every possible hypothesis. *)
-
-Ltac simpl_JMeq := repeat simpl_one_JMeq.
-
-(** Just simplify an h.eq. without clearing it. *)
-
-Ltac simpl_one_dep_JMeq :=
-  on_JMeq
-  ltac:(fun H => let H' := fresh "H" in 
-    assert (H' := JMeq_eq H)).
-
-
-
-
diff --git a/contrib/subtac/Subtac.v b/contrib/subtac/Subtac.v
deleted file mode 100644
index 9912cd242c..0000000000
--- a/contrib/subtac/Subtac.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Require Export Coq.subtac.Utils.
-Require Export Coq.subtac.FixSub.
\ No newline at end of file
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index e774dd127a..d38bdb79ef 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -95,8 +95,8 @@ let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
 (*   check_required_library ["Coq";"Logic";"JMeq"]; *)
-  require_library "Coq.subtac.FixSub";
-  require_library "Coq.subtac.Utils";
+  require_library "Coq.Program.FixSub";
+  require_library "Coq.Program.Tactics";
   require_library "Coq.Logic.JMeq";
   let env = Global.env () in
   let isevars = ref (create_evar_defs Evd.empty) in
@@ -125,6 +125,10 @@ let subtac (loc, command) =
       | VernacAssumption (stre,nl,l) -> 
 	  vernac_assumption env isevars stre l nl
 
+(*       | VernacCoFixpoint (l, b) ->  *)
+(* 	  let _ = trace (str "Building cofixpoint") in *)
+(* 	    ignore(Subtac_command.build_recursive l b) *)
+
       (*| VernacEndProof e -> 
 	  subtac_end_proof e*)
 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 1bd85b92bd..656c4397d3 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -13,7 +13,7 @@ open Decl_kinds
 open Util
 open Evd
 
-let pperror cmd = Util.errorlabstrm "Subtac" cmd
+let pperror cmd = Util.errorlabstrm "Program" cmd
 let error s = pperror (str s)
 
 exception NoObligations of identifier option
@@ -96,7 +96,7 @@ let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
 let freeze () = !from_prg, !default_tactic_expr
 let unfreeze (v, t) = from_prg := v; set_default_tactic t
 let init () =
-  from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.utils_call "subtac_simpl" [])
+  from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "program_simpl" [])
 
 let _ = 
   Summary.declare_summary "program-tcc-table"
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index b557b40569..e5ac65878d 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -10,7 +10,7 @@ let ($) f x = f x
 (****************************************************************************)
 (* Library linking *)
 
-let contrib_name = "subtac"
+let contrib_name = "Program"
 
 let subtac_dir = [contrib_name]
 let fix_sub_module = "FixSub"
@@ -28,8 +28,8 @@ let make_ref l s = lazy (init_reference l s)
 let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
 let acc_ref = make_ref  ["Init";"Wf"] "Acc"
 let acc_inv_ref = make_ref  ["Init";"Wf"] "Acc_inv"
-let fix_sub_ref = make_ref ["subtac";"FixSub"] "Fix_sub"
-let fix_measure_sub_ref = make_ref ["subtac";"FixSub"] "Fix_measure_sub"
+let fix_sub_ref = make_ref [contrib_name;"FixSub"] "Fix_sub"
+let fix_measure_sub_ref = make_ref [contrib_name;"FixSub"] "Fix_measure_sub"
 let lt_ref = make_ref ["Init";"Peano"] "lt"
 let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf"
 let refl_ref = make_ref ["Init";"Logic"] "refl_equal"
@@ -441,11 +441,11 @@ let pr_evar_defs evd =
       str"METAS:"++brk(0,1)++pr_meta_map evd in
   v 0 (pp_evm ++ pp_met)
 
-let subtac_utils_path =
-  make_dirpath (List.map id_of_string ["Utils";contrib_name;"Coq"])
-let utils_tac s =
-  lazy(make_kn (MPfile subtac_utils_path) (make_dirpath []) (mk_label s))
+let contrib_tactics_path =
+  make_dirpath (List.map id_of_string ["Tactics";contrib_name;"Coq"])
+let tactics_tac s =
+  lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s))
 
-let utils_call tac args =
-  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (utils_tac tac)),args))
+let tactics_call tac args =
+  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args))
 
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 5a5dd4274b..bbf536c41f 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -125,6 +125,6 @@ val string_of_intset : Intset.t -> string
 
 val pr_evar_defs : evar_defs -> Pp.std_ppcmds
 
-val utils_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr
+val tactics_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr
 
 val pp_list : ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds
diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex
index 0d5017f8ba..ecb872b0e8 100644
--- a/doc/refman/RefMan-ind.tex
+++ b/doc/refman/RefMan-ind.tex
@@ -502,7 +502,7 @@ conjunction of their conclusions. For exemple, we can combine the
 induction principles for trees and forests:
 
 \begin{coq_example*}
-Mutual Scheme tree_forest_mutind from tree_ind, forest_ind.
+Combined Scheme tree_forest_mutind from tree_ind, forest_ind.
 Check tree_forest_mutind.
 \end{coq_example*}
 
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 6022da116c..1915ad37cb 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -14,4 +14,4 @@ Require Export Datatypes.
 Require Export Specif.
 Require Export Peano.
 Require Export Wf.
-Require Export Tactics.
+Require Export Coq.Init.Tactics.
diff --git a/contrib/subtac/FixSub.v b/theories/Program/FixSub.v
index f047b729dd..58ac9d90ee 100644
--- a/contrib/subtac/FixSub.v
+++ b/theories/Program/FixSub.v
@@ -1,5 +1,6 @@
 Require Import Wf.
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Utils.
+Require Import ProofIrrelevance.
 
 (** Reformulation of the Wellfounded module using subsets where possible. *)
 
diff --git a/contrib/subtac/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
index 4610f3467a..c6e5a64fb3 100644
--- a/contrib/subtac/FunctionalExtensionality.v
+++ b/theories/Program/FunctionalExtensionality.v
@@ -1,3 +1,8 @@
+Require Import Coq.Program.Utils.
+Require Import Coq.Program.FixSub.
+
+(** The converse of functional equality. *)
+
 Lemma equal_f : forall A B : Type, forall (f g : A -> B), 
   f = g -> forall x, f x = g x.
 Proof.
@@ -6,16 +11,20 @@ Proof.
   auto.
 Qed.
 
+(** Statements of functional equality for simple and dependent functions. *)
+
 Axiom fun_extensionality : forall A B (f g : A -> B), 
   (forall x, f x = g x) -> f = g.
 
 Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), forall (f g : forall x : A, B x), 
   (forall x, f x = g x) -> f = g.
 
-Hint Resolve fun_extensionality fun_extensionality_dep : subtac.
+Hint Resolve fun_extensionality fun_extensionality_dep : program.
+
+(** The two following lemmas allow to unfold a well-founded fixpoint definition without
+   restriction using the functional extensionality axiom. *)
 
-Require Import Coq.subtac.Utils.
-Require Import Coq.subtac.FixSub.
+(** For a function defined with Program using a well-founded order. *)
 
 Lemma fix_sub_eq_ext :
   forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R)
@@ -32,6 +41,8 @@ Proof.
   rewrite H0 ; auto.
 Qed.
 
+(** For a function defined with Program using a measure. *)
+
 Lemma fix_sub_measure_eq_ext :
   forall (A : Type) (f : A -> nat) (P : A -> Type)
     (F_sub : forall x : A, (forall  {y : A | f y < f x}, P (`y)) -> P x),
@@ -45,3 +56,10 @@ Proof.
   apply (fun_extensionality_dep _ _ _ _ H).
   rewrite H0 ; auto.
 Qed.
+
+Ltac apply_ext :=
+  match goal with 
+    [ |- ?x = ?y ] => apply (@fun_extensionality _ _ x y)
+  end.
+
+
diff --git a/theories/Program/Heq.v b/theories/Program/Heq.v
new file mode 100644
index 0000000000..cd405219f6
--- /dev/null
+++ b/theories/Program/Heq.v
@@ -0,0 +1,63 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: Permut.v 9245 2006-10-17 12:53:34Z notin $ i*)
+
+(** Tactics related to (dependent) equality and proof irrelevance. *)
+
+Require Export ProofIrrelevance.
+Require Export JMeq.
+
+(** 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).
+
+(** Do something on an heterogeneous equality appearing in the context. *)
+
+Ltac on_JMeq tac := 
+  match goal with
+    | [ H : @JMeq ?x ?X ?y ?Y |- _ ] => tac H
+  end.
+
+(** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *)
+
+Ltac simpl_one_JMeq :=
+  on_JMeq 
+  ltac:(fun H => let H' := fresh "H" in 
+    assert (H' := JMeq_eq H) ; clear H ; rename H' into H).
+
+(** Repeat it for every possible hypothesis. *)
+
+Ltac simpl_JMeq := repeat simpl_one_JMeq.
+
+(** Just simplify an h.eq. without clearing it. *)
+
+Ltac simpl_one_dep_JMeq :=
+  on_JMeq
+  ltac:(fun H => let H' := fresh "H" in 
+    assert (H' := JMeq_eq H)).
+
+Require Import Eqdep.
+
+(** Tries to eliminate a call to [eq_rect] (the substitution principle) by any means available. *)
+
+Ltac elim_eq_rect :=
+  match goal with
+    | [ |- ?t ] => 
+      match t with
+        | context [ @eq_rect _ _ _ _ _ ?p ] => 
+          let P := fresh "P" in 
+            set (P := p); simpl in P ; 
+	      ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
+        | context [ @eq_rect _ _ _ _ _ ?p _ ] => 
+          let P := fresh "P" in 
+            set (P := p); simpl in P ; 
+	      ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
+      end
+  end.
+
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
new file mode 100644
index 0000000000..4dc50694fa
--- /dev/null
+++ b/theories/Program/Program.v
@@ -0,0 +1,3 @@
+Require Export Coq.Program.Utils.
+Require Export Coq.Program.FixSub.
+Require Export Coq.Program.Heq.
\ No newline at end of file
diff --git a/contrib/subtac/SubtacTactics.v b/theories/Program/Tactics.v
index a00234dde8..d5ccdf1c5b 100644
--- a/contrib/subtac/SubtacTactics.v
+++ b/theories/Program/Tactics.v
@@ -1,24 +1,16 @@
-Ltac induction_with_subterm c H :=
-  let x := fresh "x" in
-  let y := fresh "y" in
-  (remember c as x ; rewrite <- y in H ; induction H ; subst).
-
-Ltac induction_on_subterm c :=
-  let x := fresh "x" in
-  let y := fresh "y" in
-  (set(x := c) ; assert(y:x = c) by reflexivity ; clearbody x ; induction x ; inversion y ; try subst ; 
-  clear y).
-
-Ltac induction_with_subterms c c' H :=
-  let x := fresh "x" in
-  let y := fresh "y" in
-  let z := fresh "z" in
-  let w := fresh "w" in
-  (set(x := c) ; assert(y:x = c) by reflexivity ;
-  set(z := c') ; assert(w:z = c') by reflexivity ;
-  rewrite <- y in H ; rewrite <- w in H ; 
-  induction H ; subst).
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
 
+(*i $Id$ i*)
+
+(** This module implements various tactics used to simplify the goals produced by Program. *)
+
+(** Destructs one pair, without care regarding naming. *)
 
 Ltac destruct_one_pair :=
  match goal with
@@ -26,8 +18,12 @@ Ltac destruct_one_pair :=
    | [H : prod _ _ |- _] => destruct H
  end.
 
+(** Repeateadly destruct pairs. *)
+
 Ltac destruct_pairs := repeat (destruct_one_pair).
 
+(** Destruct one existential package, keeping the name of the hypothesis for the first component. *)
+
 Ltac destruct_one_ex :=
   let tac H := let ph := fresh "H" in destruct H as [H ph] in
     match goal with
@@ -36,37 +32,49 @@ Ltac destruct_one_ex :=
       | [H : (ex2 _) |- _] => tac H
     end.
 
+(** Repeateadly destruct existentials. *)
+
 Ltac destruct_exists := repeat (destruct_one_ex).
 
+(** Repeateadly destruct conjunctions and existentials. *)
+
+Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex).
+
+(** Destruct an existential hypothesis [t] keeping its name for the first component 
+   and using [Ht] for the second *)
+
 Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht].
 
-Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H].
+(** Destruct a disjunction keeping its name in both subgoals. *)
 
-Tactic Notation "contradiction" "by" constr(t) := 
-  let H := fresh in assert t as H by auto with * ; contradiction.
+Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H].
 
+(** Discriminate that also work on a [x <> x] hypothesis. *)
 Ltac discriminates :=
   match goal with
     | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity
     | _ => discriminate
   end.
 
-Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex).
-
-Ltac on_last_hyp tac := 
-  match goal with
-    [ H : _ |- _ ] => tac H
-  end.
-
-Tactic Notation "on_last_hyp" tactic(t) := on_last_hyp t.
+(** Revert the last hypothesis. *)
 
 Ltac revert_last := 
   match goal with
     [ H : _ |- _ ] => revert H
   end.
 
+(** Reapeateadly reverse the last hypothesis, putting everything in the goal. *)
+
 Ltac reverse := repeat revert_last.
 
+(** A non-failing subst that substitutes as much as possible. *)
+
+Tactic Notation "subst" "*" :=
+  repeat (match goal with 
+            [ H : ?X = ?Y |- _ ] => subst X || subst Y                  
+          end).
+
+(** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *)
 Ltac on_call f tac :=
   match goal with
     | H : ?T |- _  =>
@@ -89,7 +97,8 @@ Ltac on_call f tac :=
       end
   end.
 
-(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *)
+(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object. *)
+
 Ltac destruct_call f :=
   let tac t := destruct t in on_call f tac.
 
@@ -97,9 +106,14 @@ Ltac destruct_call_as f l :=
   let tac t := destruct t as l in on_call f tac.
 
 Tactic Notation "destruct_call" constr(f) := destruct_call f.
+
+(** Permit to name the results of destructing the call to [f]. *)
+
 Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := destruct_call_as f l.
 
-Ltac myinjection :=
+(** Try to inject any potential constructor equality hypothesis. *)
+
+Ltac autoinjection :=
   let tac H := inversion H ; subst ; clear H in
     match goal with
       | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H
@@ -111,11 +125,14 @@ Ltac myinjection :=
       | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H
       | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H
       | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H
-      | _ => idtac
     end.
 
+(** Destruct an hypothesis by first copying it to avoid dependencies. *)
+
 Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0.
 
+(** If bang appears in the goal, it means that we have a proof of False and the goal is solved. *)
+
 Ltac bang :=
   match goal with
     | |- ?x => 
@@ -123,36 +140,26 @@ Ltac bang :=
         | context [False_rect _ ?p] => elim p
       end
   end.
+ 
+(** A tactic to show contradiction by first asserting an automatically provable hypothesis. *)
+Tactic Notation "contradiction" "by" constr(t) := 
+  let H := fresh in assert t as H by auto with * ; contradiction.
 
-Require Import Eqdep.
+(** 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 manner similar to 
+   the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
 
-Ltac elim_eq_rect :=
-  match goal with
-    | [ |- ?t ] => 
-      match t with
-        | context [ @eq_rect _ _ _ _ _ ?p ] => 
-          let P := fresh "P" in 
-            set (P := p); simpl in P ; 
-	      try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
-        | context [ @eq_rect _ _ _ _ _ ?p _ ] => 
-          let P := fresh "P" in 
-            set (P := p); simpl in P ; 
-	      try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
-      end
-  end.
+Tactic Notation "dependent" "induction" ident(H) := 
+  generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; 
+    induction H ; intros ; subst* ; try discriminates.
 
-Ltac real_elim_eq_rect :=
-  match goal with
-    | [ |- ?t ] => 
-      match t with
-        | context [ @eq_rect _ _ _ _ _ ?p ] => 
-          let P := fresh "P" in 
-            set (P := p); simpl in P ; 
-	      ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
-        | context [ @eq_rect _ _ _ _ _ ?p _ ] => 
-          let P := fresh "P" in 
-            set (P := p); simpl in P ; 
-	      ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
-      end
-  end.
- 
\ No newline at end of file
+(** This tactic also generalizes the goal by the given variables before the induction. *)
+
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
+  generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; 
+    generalize l ; clear l ; induction H ; intros ; subst* ; try discriminates.
+
+(** The default simplification tactic used by Program. *)
+
+Ltac program_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; 
+  try (solve [ red ; intros ; discriminate ]) ; auto with *.  
diff --git a/contrib/subtac/Utils.v b/theories/Program/Utils.v
index 76f49dd3bc..a87eda0a26 100644
--- a/contrib/subtac/Utils.v
+++ b/theories/Program/Utils.v
@@ -1,4 +1,14 @@
-Require Export Coq.subtac.SubtacTactics.
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export Coq.Program.Tactics.
 
 Set Implicit Arguments.
 
@@ -46,12 +56,8 @@ Notation "'dec'" := (sumbool_of_bool) (at level 0).
 Notation in_right := (@right _ _ _).
 Notation in_left := (@left _ _ _).
 
-(** Default simplification tactic. *)
-
-Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; 
-  try (solve [ red ; intros ; discriminate ]) ; auto with *.  
-
 (** Extraction directives *)
+
 Extraction Inline proj1_sig.
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
@@ -59,7 +65,6 @@ Extract Inductive sumbool => "bool" [ "true" "false" ].
 (* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *)
 (* Extract Inductive sigT => "prod" [ "" ]. *)
 
-Require Export ProofIrrelevance.
-Require Export Coq.subtac.Heq.
+(** The scope in which programs are typed (not their types). *)
 
-Delimit Scope program_scope with program.
+Delimit Scope program_scope with prg.