From 47b05fc01cfc977201f84d1af1e1415f84cf39dc Mon Sep 17 00:00:00 2001
From: clrenard
Date: Tue, 10 Jul 2001 12:04:17 +0000
Subject: Changement de place de la tactique Setoid_rewrite et renommage en
 Rewrite. Le choix entre egalite de Leibnitz et egalite de setoide est fait
 automatiquement

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1841 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2b1c9da35c..7b319b48d1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -33,6 +33,7 @@ open Tacinterp
 open Tacred
 open Vernacinterp
 open Coqlib
+open Setoid_replace
 
 (* Rewriting tactics *)
 
@@ -50,7 +51,10 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
   let sigma = project gl in 
   let _,t = splay_prod env sigma ctype in
   match match_with_equation t with
-    | None -> error "The term provided does not end with an equation" 
+    | None -> 
+	if l = []
+	then general_s_rewrite lft2rgt c gl
+	else error "The term provided does not end with an equation" 
     | Some (hdcncl,_) -> 
         let hdcncls = string_head hdcncl in 
 	let suffix = Declare.elimination_suffix (sort_of_goal gl) in
-- 
cgit v1.2.3