From d723362607c3746944f2a67ecc58601b2ab64be3 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Thu, 30 Sep 2004 11:39:17 +0000
Subject: cutrewrite does not work with relations that are not Coq-like
 equalities. Thus it does not work for setoid relations and it can replace
 setoid_replace when the user wants to specify what the relation should be.

To solve the problem this commit enables the syntax

setoid_replace E1 with E2 using relation R ...


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6163 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/setoid_replace.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tactics/setoid_replace.mli')

diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index 5e08ffeaab..0a8405d039 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -23,7 +23,8 @@ val print_setoids : unit -> unit
 
 val equiv_list : unit -> constr list
 
-val setoid_replace : constr -> constr -> new_goals:constr list -> tactic
+val setoid_replace :
+ constr option -> constr -> constr -> new_goals:constr list -> tactic
 
 val general_s_rewrite : bool -> constr -> new_goals:constr list -> tactic
 
-- 
cgit v1.2.3