diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 12:22:29 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-15 11:58:21 +0100 |
| commit | 78896394b49b0d8b89c81378f9437e69a86b6363 (patch) | |
| tree | 3c28f3a2c416d32c23c654cbba68f911dbc4b731 /tactics | |
| parent | 1aecaf88e5491d29b200515fc64ce3d479318758 (diff) | |
Granting clear_flag in injection, even legacy mode. This is possible
since the clear_flag is new.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 89d14fdc7..92ebcb272 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 = |