From 91e9e1c26b7f2b874df83600b2bc8d23df9ed48b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Dec 2016 19:45:04 +0100
Subject: Passing around the flag for injection so that tactics calling inj at
 ML level can set the flags themselves.

In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".

This fixes bug #5281.
---
 plugins/ssr/ssrelim.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 832044909c..26b5c57675 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)
-- 
cgit v1.2.3