diff options
| author |  Théo Zimmermann <theo.zimmi@gmail.com> | 2016-10-01 08:37:59 +0200 |
|---|---|---|
| committer |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-10-01 09:07:04 +0200 |
| commit | cc407dc4272928944af06ee141d71ff3c9622347 (patch) | |
| tree | 5bd2bcf74f0675e86cd6864e520b4cad167b25bb /tactics | |
| parent | 064de6f6839c4ef963b83018812c5d4113eb2bb9 (diff) | |
Micro refactoring: use exact_no_check.
This does not affect the semantics of these functions.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c550df101..c8cdae53b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1937,9 +1937,7 @@ let exact_check c = let cast_no_check cast c = Proofview.Goal.enter { enter = begin fun gl -> let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in - Refine.refine ~unsafe:true { run = begin fun sigma -> - Sigma.here (Term.mkCast (c, cast, concl)) sigma - end } + exact_no_check (Term.mkCast (c, cast, concl)) end } let vm_cast_no_check c = cast_no_check Term.VMcast c @@ -1976,7 +1974,7 @@ let assumption = in if is_same_type then (Proofview.Unsafe.tclEVARS sigma) <*> - Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h } + exact_no_check (mkVar (get_id decl)) else arec gl only_eq rest in let assumption_tac = { enter = begin fun gl -> |