From 78896394b49b0d8b89c81378f9437e69a86b6363 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 10 Dec 2015 12:22:29 +0100
Subject: Granting clear_flag in injection, even legacy mode. This is possible
 since the clear_flag is new.

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 89d14fdc7b..92ebcb2724 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1356,7 +1356,7 @@ let postInjEqTac clear_flag ipats c n =
         then intro_patterns_bound_to n MoveLast ipats
         else intro_patterns_to MoveLast ipats in
       tclTHEN clear_tac intro_tac
-  | None -> tclIDTAC
+  | None -> apply_clear_request clear_flag false c
 
 let injEq clear_flag ipats =
   let l2r =
-- 
cgit v1.2.3