diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-08 13:06:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-08 13:49:54 +0200 |
| commit | 76f27140e6e3465b2d4086653bccae5206b3cfb6 (patch) | |
| tree | c85c82d533189eaebd00b28eec07f49c5b630960 /tactics | |
| parent | 46bd7186b1236da4ef4f3e608ee989ca77d699ab (diff) | |
Fixing clearing of temporary hypotheses with intro pattern pat/constr.
Diffstat (limited to 'tactics')
| -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 |