aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrelim.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 832044909..26b5c5767 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -396,7 +396,7 @@ let revtoptac n0 gl =
let equality_inj l b id c gl =
let msg = ref "" in
- try Proofview.V82.of_tactic (Equality.inj l b None c) gl
+ try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
with
| Ploc.Exc(_,CErrors.UserError (_,s))
| CErrors.UserError (_,s)