diff options
| -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 4f7a6188a7..1e3eda0328 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 -> |