diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-07 00:28:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-07 01:20:25 +0200 |
| commit | 24a0df63c1844c6f2c69f9644a3059d668fd1e6f (patch) | |
| tree | 950372175994d0f5211b984a63bfee039cac4ebe /proofs/refiner.ml | |
| parent | e6a7182526a47f4010274128c30407ed57e51339 (diff) | |
Adding a new Control file centralizing the control options of Coq.
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 157faae3d..f0e8bf3ec 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -44,7 +44,7 @@ let unpackage glsig = (ref (glsig.sigma)), glsig.it let repackage r v = {it = v; sigma = !r; } let apply_sig_tac r tac g = - check_for_interrupt (); (* Breakpoint *) + Control.check_for_interrupt (); (* Breakpoint *) let glsigma = tac (repackage r g) in r := glsigma.sigma; glsigma.it @@ -219,10 +219,10 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) let catch_failerror e = - if catchable_exception e then check_for_interrupt () + if catchable_exception e then Control.check_for_interrupt () else match e with | FailError (0,_) -> - check_for_interrupt () + Control.check_for_interrupt () | FailError (lvl,s) -> raise (Exninfo.copy e (FailError (lvl - 1, s))) | e -> raise e |