1 files changed, 32 insertions, 29 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 72a1267c3..b1f0360c4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -119,36 +119,39 @@ let general_rewrite_bindings_in l2r id =
 let general_rewrite_in l2r id c = 
   general_rewrite_bindings_clause (Some id) l2r (c,NoBindings)
 
-
 let general_multi_rewrite l2r c cl = 
-  let rec do_hyps = function 
-    | [] -> tclIDTAC
-    | ((_,id),_) :: l -> 
-	tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l)
-  in 
-  let rec try_do_hyps = function 
-    | [] -> tclIDTAC 
-    | id :: l -> 
-	tclTHENFIRST 
-	  (tclTRY (general_rewrite_bindings_in l2r id c)) 
-	  (try_do_hyps l)
-  in 
-    if cl.concl_occs <> [] then 
-      error "The \"at\" syntax isn't available yet for the rewrite/replace tactic"
-    else 
-      tclTHENFIRST 
-	(if cl.onconcl then general_rewrite_bindings l2r c else tclIDTAC)
-	(match cl.onhyps with 
-	   | Some l -> do_hyps l
-	   | None -> 
-	       fun gl -> 
-		 (* try to rewrite in all hypothesis 
-		    (except maybe the rewritten one) *)
-		 let ids = match kind_of_term (fst c) with 
-		   | Var id -> list_remove id (pf_ids_of_hyps gl)
-		   | _ -> pf_ids_of_hyps gl
-		 in try_do_hyps ids gl)
-
+  if cl.concl_occs <> [] then 
+    error "The \"at\" syntax isn't available yet for the rewrite/replace tactic"
+  else match cl.onhyps with 
+    | Some l -> 
+	(* If a precise list of locations is given, success is mandatory for
+	   each of these locations. *)
+	let rec do_hyps = function 
+	  | [] -> tclIDTAC
+	  | ((_,id),_) :: l -> 
+	      tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l)
+	in 
+	if not cl.onconcl then do_hyps l 
+	else tclTHENFIRST (general_rewrite_bindings l2r c) (do_hyps l)
+    | None -> 
+	(* Otherwise, if we are told to rewrite in all hypothesis via the 
+           syntax "* |-", we fail iff all the different rewrites fail *) 
+	let rec do_hyps_atleastonce = function 
+	  | [] -> (fun gl -> error "Nothing to rewrite.")
+	  | id :: l -> 
+	      tclIFTHENTRYELSEMUST 
+		(general_rewrite_bindings_in l2r id c) 
+		(do_hyps_atleastonce l)
+	in 
+	let do_hyps gl = 
+	  (* If the term to rewrite is an hypothesis, don't rewrite in itself *)
+	  let ids = match kind_of_term (fst c) with 
+	    | Var id -> list_remove id (pf_ids_of_hyps gl)
+	    | _ -> pf_ids_of_hyps gl
+	  in do_hyps_atleastonce ids gl
+	in 
+	if not cl.onconcl then do_hyps 
+	else tclIFTHENTRYELSEMUST (general_rewrite_bindings l2r c) do_hyps
 
 (* Conditional rewriting, the success of a rewriting is related 
    to the resolution of the conditions by a given tactic *)