Backtrack changes on eauto, move specialized version of eauto in

class_tactics for further customizations. Add Equivalence.v for
typeclass definitions on equivalences and clrewrite.v test-suite for
clrewrite. Debugging the tactic I found missing morphisms that are now
in Morphisms.v and removed some that made proof search fail or take too
long, not sure it's complete however.


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

1 files changed, 0 insertions, 95 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index effebf331..706ba9840 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -226,7 +226,6 @@ let find_first_goal gls =
 
 (*s The following module [SearchProblem] is used to instantiate the generic
     exploration functor [Explore.Make]. *)
-      
 
 type search_state = { 
   depth : int; (*r depth of search before failing *)
@@ -339,13 +338,6 @@ let make_initial_state n gl dblist localdb =
     dblist = dblist;
     localdb = [localdb] }
 
-let make_initial_state_gls n gls dblist localdbs =
-  { depth = n;
-    tacres = gls;
-    last_tactic = (mt ());
-    dblist = dblist;
-    localdb = localdbs }
-
 let debug_depth_first = Search.debug_depth_first
 
 let e_depth_search debug p db_list local_db gl =
@@ -355,13 +347,6 @@ let e_depth_search debug p db_list local_db gl =
     s.tacres
   with Not_found -> error "EAuto: depth first search failed"
 
-let e_depth_search_gls debug p db_list local_dbs gls =
-  try
-    let tac = if debug then Search.debug_depth_first else Search.depth_first in
-    let s = tac (make_initial_state_gls p gls db_list local_dbs) in
-    s.tacres
-  with Not_found -> error "EAuto: depth first search failed"
-
 let e_breadth_search debug n db_list local_db gl =
   try
     let tac = 
@@ -371,15 +356,6 @@ let e_breadth_search debug n db_list local_db gl =
     s.tacres
   with Not_found -> error "EAuto: breadth first search failed"
 
-let e_breadth_search_gls debug n db_list local_dbs gls =
-  try
-    let tac = 
-      if debug then Search.debug_breadth_first else Search.breadth_first 
-    in
-    let s = tac (make_initial_state_gls n gls db_list local_dbs) in
-    s.tacres
-  with Not_found -> error "EAuto: breadth first search failed"
-
 let e_search_auto debug (in_depth,p) lems db_list gl = 
   let local_db = make_local_hint_db lems gl in 
   if in_depth then 
@@ -389,14 +365,6 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
 
 open Evd
 
-let e_search_auto_gls debug (in_depth,p) lems db_list gls = 
-  let sigma = Evd.sig_sig (fst gls) and gls' = Evd.sig_it (fst gls) in
-  let local_dbs = List.map (fun gl -> make_local_hint_db lems ({it = gl; sigma = sigma})) gls' in
-  if in_depth then 
-    e_depth_search_gls debug p db_list local_dbs gls
-  else
-    e_breadth_search_gls debug p db_list local_dbs gls
-
 let eauto debug np lems dbnames =
   let db_list =
     List.map
@@ -413,12 +381,6 @@ let full_eauto debug n lems gl =
   let db_list = List.map searchtable_map dbnames in
   tclTRY (e_search_auto debug n lems db_list) gl
 
-let full_eauto_gls debug n lems gls = 
-  let dbnames = current_db_names () in
-  let dbnames =  list_subtract dbnames ["v62"] in
-  let db_list = List.map searchtable_map dbnames in
-    e_search_auto_gls debug n lems db_list gls
-
 let gen_eauto d np lems = function
   | None -> full_eauto d np lems
   | Some l -> eauto d np lems l
@@ -482,60 +444,3 @@ TACTIC EXTEND dfs_eauto
       hintbases(db) ] ->
     [ gen_eauto false (true, make_depth p) lems db ]
 END
-
-open Evd
-
-exception Found of evar_defs
-
-let valid evm p res_sigma l = 
-  let evd' =
-    Evd.fold
-      (fun ev evi (gls, sigma) ->
-	if not (Evd.is_evar evm ev) then
-	  match gls with
-	      hd :: tl -> 
-		if evi.evar_body = Evar_empty then
-		  let cstr, obls = Refiner.extract_open_proof !res_sigma hd in
-		    (tl, Evd.evar_define ev cstr sigma)
-		else (tl, sigma)
-	    | [] -> ([], sigma)
-	else if not (Evd.is_defined evm ev) && p ev evi then
-	  match gls with
-	      hd :: tl -> 
-		if evi.evar_body = Evar_empty then
-		  let cstr, obls = Refiner.extract_open_proof !res_sigma hd in
-		    (tl, Evd.evar_define ev cstr sigma)
-		else (tl, sigma)
-	    | [] -> assert(false)
-	else (gls, sigma))
-      !res_sigma (l, Evd.create_evar_defs !res_sigma)
-  in raise (Found (snd evd'))
-    
-let resolve_all_evars_once debug (mode, depth) env p evd =
-  let evm = Evd.evars_of evd in
-  let goals = 
-    Evd.fold
-      (fun ev evi gls ->
-	if evi.evar_body = Evar_empty && p ev evi then
-	  (evi :: gls)
-	else gls)
-      evm []
-  in
-  let gls = { it = List.rev goals; sigma = evm } in
-  let res_sigma = ref evm in
-  let gls', valid' = full_eauto_gls debug (mode, depth) [] (gls, valid evm p res_sigma) in
-    res_sigma := Evarutil.nf_evars (sig_sig gls');
-    try ignore(valid' []); assert(false) with Found evd' -> Evarutil.nf_evar_defs evd'
-
-let has_undefined p evd =
-  Evd.fold (fun ev evi has -> has ||
-    (evi.evar_body = Evar_empty && p ev evi))
-    (Evd.evars_of evd) false
-    
-let rec resolve_all_evars debug m env p evd =
-  let rec aux n evd = 
-    if has_undefined p evd && n > 0 then
-      let evd' = resolve_all_evars_once debug m env p evd in
-	aux (pred n) evd'
-    else evd
-  in aux 3 evd