diff options
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 661a786b0..3d6928d03 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2172,7 +2172,7 @@ and intro_pattern_action loc b style pat thin tac id = match pat with (Tacticals.New.tclTHENFIRST (* Skip the side conditions of the apply *) (apply_in_once false true true true naming id - (None,(sigma,(c,NoBindings))) tac_ipat) (tac thin None [])) + (None,(sigma,(c,NoBindings))) tac_ipat) (tac ((dloc,id)::thin) None [])) sigma end |