diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-01-31 15:05:38 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-01-31 18:30:00 +0100 |
| commit | 2ea5251fa8e203d5d5b9a1eb3f6887bafdabe155 (patch) | |
| tree | 62d0d5d129c1fade6f109e0f1e861c75b5bd455f | |
| parent | 07d63bf9af363e4924ca14cb88b723c8ed2ea2dc (diff) | |
In Ltac's exact tactic: avoid checking the type of the term twice.
Following a remark by Jason Gross and Daniel Grayson.
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 4f7a6188a..1e3eda032 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1472,7 +1472,7 @@ and interp_atomic ist tac = let (sigma,c_interp) = pf_interp_casted_constr ist gl c in tclTHEN (tclEVARS sigma) - (Tactics.exact_check c_interp) + (Tactics.exact_no_check c_interp) gl end | TacExactNoCheck c -> |