Fichiers tactics/*.ml4 remplacent les tactics/*.v

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

8 files changed, 0 insertions, 848 deletions

diff --git a/tactics/AutoRewrite.v b/tactics/AutoRewrite.v
deleted file mode 100644
index 74e6d4d26..000000000
--- a/tactics/AutoRewrite.v
+++ /dev/null
@@ -1,33 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-Declare ML Module "autorewrite".
-
-Grammar vernac orient : ast :=
-| lr ["->"] -> ["LR"]
-| rl ["<-"] -> ["RL"]
-| ng [] -> ["LR"]
-
-with vernac : ast :=
-| hint_rew_b [ "Hint" "Rewrite" orient($o) "[" ne_constrarg_list($l) "]" "in"
-  identarg($b) "."] ->
-  [ (HintRewrite $o (CONSTRLIST ($LIST $l)) $b (TACTIC (Idtac))) ]
-| hint_rew_t [ "Hint" "Rewrite" orient($o) "[" ne_constrarg_list($l) "]" "in"
-  identarg($b) "using" tacarg($t) "." ] ->
-  [ (HintRewrite $o (CONSTRLIST ($LIST $l)) $b (TACTIC $t)) ].
-
-Grammar tactic simple_tactic : ast :=
-| auto_rew_b [ "AutoRewrite" "[" ne_identarg_list($l) "]" ] ->
-  [ (AutoRewrite ($LIST $l)) ]
-| auto_rew_t [ "AutoRewrite" "[" ne_identarg_list($l) "]" "using"
-  tactic($t) ] -> [ (AutoRewrite (TACTIC $t) ($LIST $l)) ].
-
-Syntax tactic level 0:
-| auto_rew_b [<<(AutoRewrite $l)>>] ->
-  [ "AutoRewrite" [1 0] "[" [1 0] $l [1 0] "]" ]
-| auto_rew_t [<<(AutoRewrite $t $l)>>] ->
-  [ "AutoRewrite" [1 0] "[" [1 0] $l [1 0] "]" [1 0] "using" [1 0] $t ].
diff --git a/tactics/EAuto.v b/tactics/EAuto.v
deleted file mode 100644
index ba233cdd3..000000000
--- a/tactics/EAuto.v
+++ /dev/null
@@ -1,80 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-(****************************************************************************)
-(*                 The Calculus of Inductive Constructions                  *)
-(*                                                                          *)
-(*                                Projet Coq                                *)
-(*                                                                          *)
-(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
-(*              Rocquencourt         Orsay          Lyon                    *)
-(*                                                                          *)
-(*                                 Coq V6.3                                 *)
-(*                               July 1st 1999                              *)
-(*                                                                          *)
-(****************************************************************************)
-(*                                 Prolog.v                                 *)
-(****************************************************************************)
-
-Grammar tactic simple_tactic: ast :=
-  eapply [ "EApply" constrarg_binding_list($cl) ]
-      -> [(EApplyWithBindings ($LIST $cl))]
-| eexact [ "EExact" constrarg($c) ] -> [(EExact $c)]
-| prolog [ "Prolog" "[" constrarg_list($l) "]" numarg($n) ]
-      -> [(Prolog $n ($LIST $l))]
-| instantiate [ "Instantiate" numarg($n) constrarg($c) ] 
-      -> [(Instantiate $n $c)]
-| normevars [ "NormEvars" ] -> [(NormEvars)]
-| etrivial [ "ETrivial" ] -> [(ETrivial)]
-| eauto [ "EAuto" eautoarg($np) ] 
-        -> [(EAuto ($LIST $np))]
-| eauto_with [ "EAuto" eautoarg($np) "with" ne_identarg_list($lid) ] 
-	-> [(EAuto ($LIST $np) ($LIST $lid))]
-| eauto_with_star [ "EAuto" eautoarg($np) "with" "*" ] 
-	-> [(EAuto ($LIST $np) "*")]
-| eautod [ "EAutod" eautoarg($np) ] 
-        -> [(EAuto "debug" ($LIST $np))]
-| eautod_with [ "EAutod" eautoarg($np) "with" ne_identarg_list($lid) ] 
-	-> [(EAuto "debug" ($LIST $np) ($LIST $lid))]
-| eautod_with_star [ "EAutod" eautoarg($np) "with" "*" ] 
-	-> [(EAuto "debug" ($LIST $np) "*")]
-
-with eautoarg : ast list :=
-| eautoarg_mt [ ] -> [ ]
-| eautoarg_n  [ numarg($n) ] -> [ $n ] 
-| eautoarg_np [ numarg($n) numarg($p) ] -> [ $n $p ] 
-.
-
-Syntax tactic level 0:
-  eauto_with [<<(EAuto ($LIST $lid))>>] -> 
-	[ "EAuto" [1 0] "with " [<hov 0> (LISTSPC ($LIST $lid))] ]
-| eauto [<<(EAuto)>>] -> ["EAuto"]
-| eauto_n_with [<<(EAuto ($NUM $n) ($LIST $lid))>>] ->
-	[ "EAuto " $n [1 0] "with " [<hov 0> (LISTSPC ($LIST $lid))] ]
-| eauto_n [<<(EAuto ($NUM $n))>>] -> ["EAuto " $n]
-| eauto_with_star [<<(EAuto "*")>>] -> 
-	[ "EAuto with *" ]
-| eauto_n_with_star [<<(EAuto ($NUM $n) "*")>>] ->
-	[ "EAuto " $n " with *" ]
-| etrivial [<<(ETrivial)>>] -> ["ETrivial"]
-
-| eexact [<<(EExact $c)>>] -> ["EExact " $c]
-
-| eapply [<<(EApplyWithBindings $c ($LIST $bl))>>]
-      -> ["EApply " $c (WITHBINDING ($LIST $bl))]
-
-| prolog [<<(Prolog ($NUM $n) ($LIST $l))>>]
-    -> [ [<hov 0> "Prolog" [1 2] "[" [<hov 0> (LISTSPC ($LIST $l)) ] "]"
-                  [1 2] $n] ]
-
-| instantiate [<<(Instantiate ($NUM $n) $c)>>] -> ["Instantiate " $n [1 2] $c]
-
-| normevars [<<(NormEvars)>>] -> ["NormEvars"].
-
-
-(* $Id$ *)
-
diff --git a/tactics/EqDecide.v b/tactics/EqDecide.v
deleted file mode 100644
index 05305d1b2..000000000
--- a/tactics/EqDecide.v
+++ /dev/null
@@ -1,40 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-(****************************************************************************)
-(*                                EqDecide.v                                *)
-(*     A tactic for deciding propositional equality on inductive types      *)
-(*                             by Eduardo Gimenez                           *)
-(****************************************************************************)
-
-(*i $Id$ i*)
-
-Declare ML Module "equality" "eqdecide".
-
-
-Grammar tactic simple_tactic : ast :=
-  EqDecideRuleG1 
-   [ "Decide"  "Equality" constrarg($com1) constrarg($com2) ] -> 
-   [ (DecideEquality $com1 $com2) ]
-
-| EqDecideRuleG2 
-   [ "Decide" "Equality" ] -> [ (DecideEquality) ]
-
-| CompareRule 
-   [ "Compare" constrarg($com1) constrarg($com2) ] -> [ (Compare $com1 $com2) ].
-
-
-Syntax tactic level 0:
-  EqDecideRulePP1 
-   [ <<(DecideEquality)>> ] -> [ "Decide Equality" ]
-
-| EqDecideRulePP2 
-   [ <<(DecideEquality $com1 $com2)>> ] -> 
-   [ "Decide Equality" [1 2] $com1 [1 2] $com2 ]
-
-| ComparePP 
-   [ <<(Compare $com1 $com2)>> ] -> [ "Compare" [1 2] $com1 [1 2] $com2 ].
diff --git a/tactics/Inv.v b/tactics/Inv.v
deleted file mode 100644
index 4f17f081b..000000000
--- a/tactics/Inv.v
+++ /dev/null
@@ -1,110 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id: *)
-
-Require Export Equality.
-
-Declare ML Module "Inv" "Leminv".
-
-Syntax tactic level 0:
-| inversion    [<<(Inv $ic $id)>>] -> [ (INVCOM $ic) [1 1] $id]
-| inversion_in [<<(InvIn $ic $id ($LIST $l))>>]
-    -> [ (INVCOM $ic) [1 1] $id (CLAUSE ($LIST $l))]
-
-| dep_inv [<<(DInv $ic $id)>>] -> ["Dependent " (INVCOM $ic) [1 1] $id]
-| dep_inv_with [<<(DInvWith $ic $id $c)>>]
-    -> ["Dependent " (INVCOM $ic) [1 1] $id [1 1] "with " $c]
-
-(* Use rules *)
-
-| inv_using
-    [<<(UseInversionLemma $id $c)>>] -> ["Inversion " $id [1 1] "using " $c]
-| inv_using_in [<<(UseInversionLemmaIn $id $c ($LIST $l))>>]
-    -> ["Inversion " $id [1 1] "using " $c (CLAUSE ($LIST $l))]
-
-| simple_inv       [<<(INVCOM "HalfInversion")>>] -> [ "Simple Inversion" ]
-| inversion_com    [<<(INVCOM "Inversion")>>] -> [ "Inversion" ]
-| inversion_clear  [<<(INVCOM "InversionClear")>>] -> [ "Inversion_clear" ].
-
-
-Grammar tactic simple_tactic: ast :=
-  inversion    [ inversion_com($ic) identarg($id) ] -> [(Inv $ic $id)]
-| inversion_num [ inversion_com($ic) pure_numarg($n) ] -> [(Inv $ic $n)]
-| inversion_in [ inversion_com($ic) identarg($id) "in" ne_identarg_list($l) ]
-      -> [(InvIn $ic $id ($LIST $l))]
-| dep_inv   [ "Dependent" inversion_com($ic) identarg($id)] -> [(DInv $ic $id)]
-| dep_inv_num  [ "Dependent" inversion_com($ic) pure_numarg($n) ] -> [(DInv $ic $n)]
-| dep_inv_with
-   [ "Dependent" inversion_com($ic) identarg($id) "with" constrarg($c) ]
-     -> [(DInvWith $ic $id $c) ]
-| dep_inv_num_with
-   [ "Dependent" inversion_com($ic) pure_numarg($n) "with" constrarg($c) ]
-     -> [(DInvWith $ic $n $c) ]
-
-| inv_using [ inversion_com($ic) identarg($id) "using" constrarg($c) ]
-     -> case [$ic] of
-          "Inversion" -> [(UseInversionLemma $id $c)]
-        esac
-
-| inv_num_using [ inversion_com($ic) pure_numarg($n) "using" constrarg($c) ]
-     -> case [$ic] of
-          Inversion -> [(UseInversionLemma $n $c)]
-        esac
-
-| inv_using_in
-   [ inversion_com($ic) identarg($id) "using" constrarg($c)
-     "in" ne_identarg_list($l) ]
-     -> case [$ic] of
-          "Inversion" -> [(UseInversionLemmaIn $id $c ($LIST $l))]
-        esac
-
-with inversion_com: ast :=
-  simple_inv    [ "Simple" "Inversion" ] -> [ "HalfInversion" ]
-| inversion_com [ "Inversion" ] -> [ "Inversion" ]
-| inv_clear     [ "Inversion_clear" ] -> [ "InversionClear" ].
-
-
-Grammar vernac vernac: ast :=
-  der_inv_clr [ "Derive" "Inversion_clear"  identarg($na) identarg($id) "." ]
-               -> [(MakeInversionLemmaFromHyp 1 $na $id)]
-
-| der_inv_clr_num [ "Derive" "Inversion_clear"
-                     numarg($n) identarg($na) identarg($id) "." ]
-                   -> [(MakeInversionLemmaFromHyp $n $na $id)]
-
-| der_inv_clr_with_srt [ "Derive" "Inversion_clear"  identarg($na) 
-                         "with" constrarg($com) "Sort" sortarg($s) "." ]
-                        -> [(MakeInversionLemma $na $com $s)]
-
-| der_inv_clr_with [ "Derive" "Inversion_clear"  identarg($na)
-                     "with" constrarg($com) "." ]
-                    -> [(MakeInversionLemma $na $com (CONSTR (PROP))) ]
-
-| der_inv_with_srt [ "Derive" "Inversion" identarg($na)
-                     "with" constrarg($com) "Sort" sortarg($s) "." ]
-                    -> [(MakeSemiInversionLemma $na $com $s)]
-
-| der_inv_with [ "Derive" "Inversion" identarg($na) "with" constrarg($com) "." ]
-                -> [(MakeSemiInversionLemma $na $com (CONSTR (PROP)))]
-
-| der_inv [ "Derive" "Inversion" identarg($na) identarg($id) "." ]
-           -> [(MakeSemiInversionLemmaFromHyp 1 $na $id)]
-
-| der_inv_num [ "Derive" "Inversion"
-                numarg($n) identarg($na) identarg($id) "." ]
-               -> [(MakeSemiInversionLemmaFromHyp $n $na $id)]
-
-| der_dep_inv_with_srt [ "Derive" "Dependent" "Inversion" identarg($na) 
-                         "with" constrarg($com) "Sort" sortarg($s) "." ]
-                  -> [(MakeDependentSemiInversionLemma $na $com $s)]
-
-| der_dep_inv_clr_with_srt
-     [ "Derive" "Dependent" "Inversion_clear"  identarg($na) 
-       "with" constrarg($com)  "Sort" sortarg($s)"." ]
-      -> [(MakeDependentInversionLemma $na $com $s)].
diff --git a/tactics/Setoid_replace.v b/tactics/Setoid_replace.v
deleted file mode 100644
index 126192758..000000000
--- a/tactics/Setoid_replace.v
+++ /dev/null
@@ -1,31 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$: *)
-
-Grammar tactic simple_tactic : ast :=
-  setoid_replace [ "Setoid_replace" constrarg($c1) "with" constrarg($c2) ] -> [(Setoid_replace $c1 $c2)]
-.
-
-Grammar tactic simple_tactic : ast :=
-  setoid_rewriteLR [ "Setoid_rewrite" "->" constrarg($c) ] -> [(Setoid_rewriteLR $c)]
-| setoid_rewriteRL [ "Setoid_rewrite" "<-" constrarg($c) ] -> [(Setoid_rewriteRL $c)]
-| setoid_rewrite [ "Setoid_rewrite" constrarg($c) ] -> [(Setoid_rewriteLR $c)]
-.
-
-Syntax tactic level 0 :
-  setoid_replace [<<(Setoid_replace  $c1 $c2)>>] -> [[<hov 0>"Setoid_replace " $c1 [1 1] "with " $c2]]
- | setoid_rewritelr [<<(Setoid_rewriteLR  $c)>>] -> ["Setoid_rewrite " $c]
- | setoid_rewriterl [<<(Setoid_rewriteRL  $c)>>] -> ["Setoid_rewrite <- " $c]
-.
-
-Grammar vernac vernac : ast :=
-  add_setoid [ "Add" "Setoid" constrarg($a) constrarg($aeq) constrarg($t) "." ] 
-    -> [(AddSetoid $a $aeq $t)]
-| new_morphism [ "Add" "Morphism" constrarg($m) ":" identarg($s) "." ] -> [(NamedNewMorphism $s $m)]
-.
diff --git a/tactics/Tauto.v b/tactics/Tauto.v
deleted file mode 100644
index e03f89685..000000000
--- a/tactics/Tauto.v
+++ /dev/null
@@ -1,22 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-Declare ML Module "tauto".
-
-Grammar tactic simple_tactic: ast :=
-  tauto [ "Tauto" ] -> [(Tauto)]
-| intuition [ "Intuition" ] -> [(Intuition)]
-| intuition_t [ "Intuition" tactic($t) ] -> [(Intuition (TACTIC $t))]
-.
-
-Syntax tactic level 0:
-  tauto [(Tauto)] -> ["Tauto"]
-| intuition [(Intuition)] -> ["Intuition"]
-| intuition_t [<<(Intuition (TACTIC $t))>>] -> ["Intuition " $t].
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
deleted file mode 100644
index f7076af25..000000000
--- a/tactics/eauto.ml
+++ /dev/null
@@ -1,335 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-open Pp
-open Util
-open Names
-open Nameops
-open Term
-open Termops
-open Sign
-open Reduction
-open Proof_type
-open Proof_trees
-open Tacmach
-open Evar_refiner
-open Tactics
-open Pattern
-open Clenv
-open Auto
-
-let e_give_exact c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in 
-  if occur_existential t1 or occur_existential t2 then 
-     tclTHEN (unify t1) (exact_no_check c) gl
-  else exact_no_check c gl
-
-let assumption id = e_give_exact (mkVar id)
-        
-let e_assumption gl = 
-  tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl
-
-let e_give_exact_constr = hide_constr_tactic "EExact" e_give_exact
-
-let registered_e_assumption gl = 
-  tclFIRST (List.map (fun id gl -> e_give_exact_constr (mkVar id) gl) 
-              (pf_ids_of_hyps gl)) gl
-    
-let e_resolve_with_bindings_tac  (c,lbind) gl = 
-  let (wc,kONT) = startWalk gl in
-  let t = w_hnf_constr wc (w_type_of wc c) in 
-  let clause = make_clenv_binding_apply wc (-1) (c,t) lbind in 
-  e_res_pf kONT clause gl
-
-let e_resolve_with_bindings = 
-  tactic_com_bind_list e_resolve_with_bindings_tac
-
-let vernac_e_resolve_with_bindings = 
-  hide_cbindl_tactic  "EApplyWithBindings" e_resolve_with_bindings_tac
-
-let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,[]) gls
-let resolve_constr c gls = Tactics.apply_with_bindings (c,[]) gls
-			     
-let vernac_e_resolve_constr = 
-  hide_constr_tactic "EApply" e_resolve_constr
-
-(************************************************************************)
-(*   PROLOG tactic                                                      *)
-(************************************************************************)
-
-let one_step l gl =
-  [Tactics.intro]
-  @ (List.map e_resolve_constr (List.map mkVar (pf_ids_of_hyps gl)))
-  @ (List.map e_resolve_constr l)
-  @ (List.map assumption (pf_ids_of_hyps gl))
-
-let rec prolog l n gl =
-  if n <= 0 then error "prolog - failure";
-  let prol = (prolog l (n-1)) in
-  (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
-
-let prolog_tac l n gl =
- (* let l = List.map (pf_interp_constr gl) lcom in *)
-  try (prolog l n gl)
-  with UserError ("Refiner.tclFIRST",_) ->
-    errorlabstrm "Prolog.prolog" (str "Prolog failed")
-
-let vernac_prolog =
-  let uncom = function
-    | Constr c -> c
-    | _ -> assert false
-  in
-  let gentac = 
-    hide_tactic "Prolog"
-      (function
-	 | (Integer n) :: al -> prolog_tac (List.map uncom al) n
-	 | _ -> assert false)
-  in 
-  fun coms n -> 
-    gentac ((Integer n) :: (List.map (fun com -> (Constr com)) coms))
-
-open Auto
-
-(***************************************************************************)
-(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
-(***************************************************************************)
-
-let unify_e_resolve  (c,clenv) gls = 
-  let (wc,kONT) = startWalk gls in
-  let clenv' = connect_clenv wc clenv in
-  let _ = clenv_unique_resolver false clenv' gls in
-  vernac_e_resolve_constr c gls
-
-let rec e_trivial_fail_db db_list local_db goal =
-  let tacl = 
-    registered_e_assumption ::
-    (tclTHEN Tactics.intro 
-       (function g'->
-	  let d = pf_last_hyp g' in
-	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
-          (e_trivial_fail_db db_list
-	     (Hint_db.add_list hintl local_db) g'))) ::
-    (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
-  in 
-  tclFIRST (List.map tclCOMPLETE tacl) goal 
-
-and e_my_find_search db_list local_db hdc concl = 
-  let hdc = head_of_constr_reference hdc in
-  let hintl =
-    if occur_existential concl then 
-      list_map_append (Hint_db.map_all hdc) (local_db::db_list)
-    else 
-      list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
-  in 
-  let tac_of_hint = 
-    fun ({pri=b; pat = p; code=t} as patac) -> 
-      (b, 
-       let tac =
-	 match t with
-	   | Res_pf (term,cl) -> unify_resolve (term,cl)
-	   | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
-	   | Give_exact (c) -> e_give_exact_constr c
-	   | Res_pf_THEN_trivial_fail (term,cl) ->
-               tclTHEN (unify_e_resolve (term,cl)) 
-		 (e_trivial_fail_db db_list local_db)
-	   | Unfold_nth c -> unfold_constr c
-	   | Extern tacast -> Tacticals.conclPattern concl 
-	       (out_some p) tacast
-       in 
-       (tac,fmt_autotactic t))
-       (*i
-	 fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); 
-                     try tac gls
-		     with e when Logic.catchable_exception(e) -> 
-                            (Format.print_string "Fail\n"; 
-			     Format.print_flush (); 
-			     raise e)
-       i*)
-  in 
-  List.map tac_of_hint hintl
-    
-and e_trivial_resolve db_list local_db gl = 
-  try 
-    Auto.priority 
-      (e_my_find_search db_list local_db 
-	 (List.hd (head_constr_bound gl [])) gl)
-  with Bound | Not_found -> []
-
-let e_possible_resolve db_list local_db gl =
-  try List.map snd (e_my_find_search db_list local_db 
-		      (List.hd (head_constr_bound gl [])) gl)
-  with Bound | Not_found -> []
-
-let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
-
-let find_first_goal gls = 
-  try first_goal gls with UserError _ -> assert false
-
-(*s The following module [SearchProblem] is used to instantiate the generic
-    exploration functor [Explore.Make]. *)
-      
-module SearchProblem = struct
-
-  type state = { 
-    depth : int; (*r depth of search before failing *)
-    tacres : goal list sigma * validation;
-    last_tactic : std_ppcmds;
-    dblist : Auto.Hint_db.t list;
-    localdb :  Auto.Hint_db.t list }
-		 
-  let success s = (sig_it (fst s.tacres)) = []
-
-  let rec filter_tactics (glls,v) = function
-    | [] -> []
-    | (tac,pptac) :: tacl -> 
-	try 
-	  let (lgls,ptl) = apply_tac_list tac glls in 
-	  let v' p = v (ptl p) in
-	  ((lgls,v'),pptac) :: filter_tactics (glls,v) tacl
-	with e when Logic.catchable_exception e ->
-	  filter_tactics (glls,v) tacl
-
-  let rec list_addn n x l = 
-    if n = 0 then l else x :: (list_addn (pred n) x l)
-
-  (* Ordering of states is lexicographic on depth (greatest first) then
-     number of remaining goals. *)
-  let compare s s' =
-    let d = s'.depth - s.depth in
-    let nbgoals s = List.length (sig_it (fst s.tacres)) in
-    if d <> 0 then d else nbgoals s - nbgoals s'
-
-  let branching s = 
-    if s.depth = 0 then 
-      []
-    else      
-      let lg = fst s.tacres in
-      let nbgl = List.length (sig_it lg) in
-      assert (nbgl > 0);
-      let g = find_first_goal lg in
-      let assumption_tacs = 
-	let l = 
-	  filter_tactics s.tacres
-	    (List.map 
-	       (fun id -> (e_give_exact_constr (mkVar id),
-			   (str "Exact" ++ spc () ++ pr_id id)))
-	       (pf_ids_of_hyps g))
-	in
-	List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
-				    last_tactic = pp; dblist = s.dblist;
-				    localdb = List.tl s.localdb }) l
-      in
-      let intro_tac = 
-	List.map 
-	  (fun ((lgls,_) as res,pp) -> 
-	     let g' = first_goal lgls in 
-	     let hintl = 
-	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
-	     in
-             let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
-	     { depth = s.depth; tacres = res; 
-	       last_tactic = pp; dblist = s.dblist;
-	       localdb = ldb :: List.tl s.localdb })
-	  (filter_tactics s.tacres [Tactics.intro,(str "Intro")])
-      in
-      let rec_tacs = 
-	let l = 
-	  filter_tactics s.tacres
-	    (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
-	in
-	List.map 
-	  (fun ((lgls,_) as res, pp) -> 
-	     let nbgl' = List.length (sig_it lgls) in
-	     if nbgl' < nbgl then
-	       { depth = s.depth; tacres = res; last_tactic = pp;
-		 dblist = s.dblist; localdb = List.tl s.localdb }
-	     else 
-	       { depth = pred s.depth; tacres = res; 
-		 dblist = s.dblist; last_tactic = pp;
-		 localdb = 
-		   list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
-	  l
-      in
-      List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
-
-  let pp s = 
-    msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++ 
-		  s.last_tactic ++ str "\n"))
-
-end
-
-module Search = Explore.Make(SearchProblem)
-
-let make_initial_state n gl dblist localdb =
-  { SearchProblem.depth = n;
-    SearchProblem.tacres = tclIDTAC gl;
-    SearchProblem.last_tactic = (mt ());
-    SearchProblem.dblist = dblist;
-    SearchProblem.localdb = [localdb] }
-
-let e_depth_search debug p db_list local_db gl =
-  try
-    let tac = if debug then Search.debug_depth_first else Search.depth_first in
-    let s = tac (make_initial_state p gl db_list local_db) in
-    s.SearchProblem.tacres
-  with Not_found -> error "EAuto: depth first search failed"
-
-let e_breadth_search debug n db_list local_db gl =
-  try
-    let tac = 
-      if debug then Search.debug_breadth_first else Search.breadth_first 
-    in
-    let s = tac (make_initial_state n gl db_list local_db) in
-    s.SearchProblem.tacres
-  with Not_found -> error "EAuto: breadth first search failed"
-
-let e_search_auto debug (n,p) db_list gl = 
-  let local_db = make_local_hint_db gl in 
-  if n = 0 then 
-    e_depth_search debug p db_list local_db gl
-  else 
-    e_breadth_search debug n db_list local_db gl
-
-let eauto debug np dbnames = 
-  let db_list =
-    List.map
-      (fun x -> 
-	 try Stringmap.find x !searchtable
-	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
-      ("core"::dbnames) 
-  in
-  tclTRY (e_search_auto debug np db_list)
-
-let full_eauto debug n gl = 
-  let dbnames = stringmap_dom !searchtable in
-  let dbnames =  list_subtract dbnames ["v62"] in
-  let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
-  let local_db = make_local_hint_db gl in
-  tclTRY (e_search_auto debug n db_list) gl
-
-let dyn_eauto l = 
-  let (debug,l) = match l with
-    | (Quoted_string "debug") :: l -> true,l
-    | _ -> false,l
-  in
-  let (np,l) = match l with
-    | (Integer n) :: (Integer p) :: l -> ((n,p),l)
-    | (Integer n) :: l -> ((n,0),l)
-    | l -> ((!default_search_depth,0),l)
-  in
-  match l with
-  | [] -> eauto debug np []
-  | [Quoted_string "*"] -> full_eauto debug np
-  | l1 -> 
-      eauto debug np 
-	(List.map (function 
-		     | Identifier id -> string_of_id id
-		     | _ -> bad_tactic_args "dyn_eauto" l) l1)
-
-let h_eauto = hide_tactic "EAuto" dyn_eauto
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
deleted file mode 100644
index be301af0e..000000000
--- a/tactics/eqdecide.ml
+++ /dev/null
@@ -1,197 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ i*)
-
-open Util
-open Names
-open Nameops
-open Term
-open Declarations
-open Tactics
-open Tacticals
-open Hiddentac
-open Equality
-open Auto
-open Pattern
-open Hipattern
-open Proof_trees
-open Proof_type
-open Tacmach
-open Coqlib
-
-(* This file containts the implementation of the tactics ``Decide
-   Equality'' and ``Compare''. They can be used to decide the
-   propositional equality of two objects that belongs to a small
-   inductive datatype --i.e., an inductive set such that all the
-   arguments of its constructors are non-functional sets.
-
-   The procedure for proving (x,y:R){x=y}+{~x=y} can be scketched as
-   follows:
-   1. Eliminate x and then y.
-   2. Try discrimination to solve those goals where x and y has
-      been introduced by different constructors.
-   3. If x and y have been introduced by the same constructor,
-      then analyse one by one the correspoing pairs of arguments.
-      If they are equal, rewrite one into the other. If they are
-      not, derive a contradiction from the injectiveness of the
-      constructor. 
-   4. Once all the arguments have been rewritten, solve the left half 
-      of the disjunction by reflexivity.
-
-   Eduardo Gimenez (30/3/98).
-*)
-
-let clear_last = (tclLAST_HYP (fun c -> (clear [destVar c])))
-
-let mkBranches = 
-  tclTHENSEQ
-    [intro; 
-     tclLAST_HYP h_simplest_elim;
-     clear_last;
-     intros ;
-     tclLAST_HYP h_simplest_case;
-     clear_last;
-     intros]
-
-let solveRightBranch  = (tclTHEN h_simplest_right h_discrConcl)
-
-let h_solveRightBranch =
-  hide_atomic_tactic "solveRightBranch" solveRightBranch
-
-
-(* Constructs the type {c1=c2}+{~c1=c2} *)
-
-let mkDecideEqGoal rectype c1 c2 g = 
-  let equality    = mkApp(build_coq_eq_data.eq (), [|rectype; c1; c2|]) in
-  let disequality = mkApp(build_coq_not (), [|equality|]) in
-  mkApp(build_coq_sumbool (), [|equality; disequality |])
-
-
-(* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *)
-
-let mkGenDecideEqGoal rectype g = 
-  let hypnames = pf_ids_of_hyps g in 
-  let xname    = next_ident_away (id_of_string "x") hypnames
-  and yname    = next_ident_away (id_of_string "y") hypnames in
-  (mkNamedProd xname rectype 
-     (mkNamedProd yname rectype 
-        (mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g)))
-
-let eqCase  tac = 
-  (tclTHEN intro  
-  (tclTHEN (tclLAST_HYP h_rewriteLR)
-  (tclTHEN clear_last 
-  tac)))
-
-let diseqCase = 
-  let diseq  = id_of_string "diseq" in
-  let absurd = id_of_string "absurd" in 
-  (tclTHEN (intro_using diseq)
-  (tclTHEN  h_simplest_right
-  (tclTHEN  red_in_concl
-  (tclTHEN  (intro_using absurd)
-  (tclTHEN  (h_simplest_apply (mkVar diseq))
-  (tclTHEN  (h_injHyp absurd)
-            full_trivial))))))
-
-let solveArg a1 a2 tac  g = 
-  let rectype = pf_type_of g a1 in
-  let decide  = mkDecideEqGoal rectype a1 a2 g in  
-  (tclTHENS
-     (h_elimType decide) 
-     [(eqCase tac);diseqCase;default_auto]) g
-
-let solveLeftBranch rectype g =
-  match
-    try matches (Coqlib.build_coq_eqdec_partial_pattern ()) (pf_concl g)
-    with Pattern.PatternMatchingFailure -> error "Unexpected conclusion!"
-  with 
-    | _ :: lhs :: rhs :: _ -> 
-        let (mib,mip) = Global.lookup_inductive rectype in
-	let nparams   = mip.mind_nparams in
-	let getargs l = snd (list_chop nparams (snd (decompose_app l))) in
-	let rargs   = getargs (snd rhs)
-	and largs   = getargs (snd lhs) in 
-	List.fold_right2 
-	  solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g
-    | _ -> anomaly "Unexpected pattern for solveLeftBranch"
-
-
-(* The tactic Decide Equality *)
-
-let hd_app c = match kind_of_term c with
-  | App (h,_) -> h
-  | _ -> c
-
-let decideGralEquality g =
-  match
-    try matches (build_coq_eqdec_pattern ()) (pf_concl g)
-    with Pattern.PatternMatchingFailure ->
-      error "The goal does not have the expected form"
-  with 
-    | (_,typ) :: _ ->
-	let headtyp = hd_app (pf_compute g typ) in
-	let rectype =
-	  match kind_of_term headtyp with
-            | Ind mi -> mi
-	    | _ -> error 
-		"This decision procedure only works for inductive objects" 
-	in 
-	(tclTHEN
-	   mkBranches 
-           (tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g
-    | _ -> anomaly "Unexpected pattern for decideGralEquality"
-
-
-let decideEquality c1 c2 g = 
-  let rectype = (pf_type_of g c1) in     
-  let decide  = mkGenDecideEqGoal rectype g in  
-  (tclTHENS (cut decide) [default_auto;decideGralEquality]) g
-
-
-(* The tactic Compare *)
-
-let compare c1 c2 g = 
-  let rectype = pf_type_of g c1 in
-  let decide  = mkDecideEqGoal rectype c1 c2 g in  
-  (tclTHENS (cut decide) 
-            [(tclTHEN  intro 
-             (tclTHEN (tclLAST_HYP simplest_case)
-                       clear_last));
-             decideEquality c1 c2]) g
-
-
-(* The dynamic tactics to be registered in the tactics table *)
-
-let dyn_decideEquality args g = match args with 
-  | [ Constr c1; Constr c2 ] -> 
-      decideEquality c1 c2 g 
-  | [ Command com1; Command com2 ] -> 
-      let c1 = pf_interp_constr g com1
-      and c2 = pf_interp_constr g com2 in  
-      decideEquality c1 c2 g 
-  | [] -> decideGralEquality g
-  | _  -> error "Invalid arguments for dynamic tactic"
-
-let dyn_compare args g = match args with 
-  | [ Constr c1; Constr c2 ] -> 
-      compare c1 c2 g
-  | [ Command com1; Command com2 ] -> 
-      let c1 = pf_interp_constr g com1
-      and c2 = pf_interp_constr g com2 in  
-      compare c1 c2 g
-  | _  ->  error "Invalid arguments for dynamic tactic"
- 
-
-(* Tactic registration *)
-
-let _ = add_tactic "DecideEquality" dyn_decideEquality
-let _ = add_tactic "Compare"        dyn_compare
-
-