Fix the clrewrite tactic, change Relations.v to work on relations in Prop

only, and get rid of the "relation" definition which makes unification
fail blatantly. Replace it with a notation :) In its current state,
the new tactic seems ready for larger tests.


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

3 files changed, 40 insertions, 23 deletions

diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4
index 84c1937ea..9aa445187 100644
--- a/tactics/class_setoid.ml4
+++ b/tactics/class_setoid.ml4
@@ -74,7 +74,8 @@ let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence")
 let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence")
 
 (* let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") *)
-let coq_relation = lazy (gen_constant ["Classes";"Relations"] "relation")
+(* let coq_relation = lazy (gen_constant ["Classes";"Relations"] "relation") *)
+let coq_relation a = mkProd (Anonymous, a, mkProd (Anonymous, a, mkProp))
 let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT")
 
 let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl")
@@ -112,7 +113,7 @@ let build_signature isevars env m cstrs finalcstr =
       (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
   in
   let mk_relty ty obj =
-    let relty = mkApp (Lazy.force coq_relation, [| ty |]) in
+    let relty = coq_relation ty in
       match obj with
 	| None -> new_evar isevars env relty
 	| Some (p, (a, r, oldt, newt)) -> r
@@ -256,17 +257,13 @@ let decompose_setoid_eqhyp gl env sigma c left2right t =
 	  let relargs, args = array_chop (Array.length args - 2) args in
 	  let rel = mkApp (r, relargs) in
 	  let typ = pf_type_of gl rel in
-	    (match kind_of_term typ with
-	      | App (relation, [| carrier |]) when eq_constr relation (Lazy.force coq_relation) 
-		    || eq_constr relation (Lazy.force coq_relationT) ->
-		  (c, (carrier, rel, args.(0), args.(1)))
-	      | _ when isArity typ ->
-		  let (ctx, ar) = destArity typ in
-		    (match ctx with
-			[ (_, None, sx) ; (_, None, sy) ] when eq_constr sx sy -> 
-			  (c, (sx, rel, args.(0), args.(1)))
-		      | _ -> error "Only binary relations are supported")
-	      | _ -> error "Not a relation")
+	    (if isArity typ then
+	      let (ctx, ar) = destArity typ in
+		(match ctx with
+		    [ (_, None, sx) ; (_, None, sy) ] when eq_constr sx sy -> 
+		      (c, (sx, rel, args.(0), args.(1)))
+		  | _ -> error "Only binary relations are supported")
+	      else error "Not a relation")
       | _ -> error "Not a relation"
   in
     if left2right then res
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 70ec9d046..da477f2a3 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -241,15 +241,19 @@ module SearchProblem = struct
 
   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 filter_tactics (glls,v) l =
+(*     let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
+    let rec aux = function
+      | [] -> []
+      | (tac,pptac) :: tacl -> 
+	  try 
+	    let (lgls,ptl) = apply_tac_list tac glls in 
+	    let v' p = v (ptl p) in
+(* 	      msg (hov 0 (pptac ++ str"\n")); *)
+	      ((lgls,v'),pptac) :: aux tacl
+	  with e when Logic.catchable_exception e ->
+	    aux tacl
+    in aux l
 
   (* Ordering of states is lexicographic on depth (greatest first) then
      number of remaining goals. *)
@@ -498,7 +502,7 @@ let valid evm p res_sigma l =
       !res_sigma (l, Evd.create_evar_defs !res_sigma)
   in raise (Found (snd evd'))
     
-let resolve_all_evars debug (mode, depth) env p evd =
+let resolve_all_evars_once debug (mode, depth) env p evd =
   let evm = Evd.evars_of evd in
   let goals = 
     Evd.fold
@@ -513,3 +517,16 @@ let resolve_all_evars debug (mode, depth) env p evd =
   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
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 940648c2e..a1ff89905 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -61,6 +61,9 @@ end
 val full_eauto_gls : bool -> bool * int -> constr list -> goal list sigma * validation -> 
   goal list sigma * validation
 
+val resolve_all_evars_once : bool -> bool * int -> env -> (evar -> evar_info -> bool) -> evar_defs ->
+  evar_defs
+
 val resolve_all_evars : bool -> bool * int -> env -> (evar -> evar_info -> bool) -> evar_defs ->
   evar_defs