diff options
| author | Julien Forest | 2014-04-04 15:58:29 +0200 |
|---|---|---|
| committer | Julien Forest | 2014-04-04 21:02:07 +0200 |
| commit | 31a69c4d0fd7b8325187e8da697a9c283594047d (patch) | |
| tree | 8f876d0abe88e2f3a3f81aa3b9d3806794e74940 /tactics | |
| parent | ba5efb7b2eac8fc4c2e166d0057f6c17f81c2fd6 (diff) | |
Closing bug #3164
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 28ca7edb57..74661b836f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -596,7 +596,7 @@ let intros_until_gen red h = Tacticals.New.tclDO n (if red then introf else intro) end -let intros_until_id id = intros_until_gen true (NamedHyp id) +let intros_until_id id = intros_until_gen false (NamedHyp id) let intros_until_n_gen red n = intros_until_gen red (AnonHyp n) let intros_until = intros_until_gen true |