aboutsummaryrefslogtreecommitdiff
path: root/tactics/equality.mli
diff options
context:
space:
mode:
authorherbelin2001-10-11 17:27:20 +0000
committerherbelin2001-10-11 17:27:20 +0000
commit301a70e45eac43f034077c95bce04edbcf2ab4ad (patch)
treed61c92f0d7a46203618a4610301c64d65c9c03ad /tactics/equality.mli
parent1d5b3f16e202af2874181671abd86a47fca37cd7 (diff)
Suppression option immediate_discharge; nettoyage de Declare et conséquences
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.mli')
-rw-r--r--tactics/equality.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 1735ebf1a0..b7ec9eb591 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -57,9 +57,6 @@ val conditional_rewrite_in :
val abstract_replace :
constr * constr -> constr * constr -> constr -> constr -> bool -> tactic
-(* Only for internal use *)
-val unsafe_replace : constr -> constr -> tactic
-
val replace : constr -> constr -> tactic
val h_replace : constr -> constr -> tactic