aboutsummaryrefslogtreecommitdiff
path: root/tactics/equality.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/equality.ml')
-rw-r--r--tactics/equality.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d78ba8c629..ec0e1d2f4e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -540,7 +540,7 @@ let replace_core clause l2r eq =
if check_setoid clause
then init_setoid ();
tclTHENFIRST
- (assert_as false None eq)
+ (assert_as false None None eq)
(onLastHypId (fun id ->
tclTHEN
(tclTRY (general_rewrite_clause l2r false (mkVar id,NoBindings) clause))