diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 17:13:38 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 18:03:29 +0200 |
| commit | d0da8a75cd1d600afa68da5e995d39a415234c2d (patch) | |
| tree | deb1a79a833756721db4db8a2b9bfdf30bcc7d7e /proofs/proof.ml | |
| parent | 56f7e0db738982684cda88a7cda833acdaa21d1f (diff) | |
Refactoring proofview: make the definition of the logic monad polymorphic.
Makes the monad more flexible as it will be easier to add new components to the concrete state of the tactic monad.
The Proofview module is also organised in a more abstract way with dedicated submodules to access various parts of the state or writer.
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 53b73097f..8d43513f2 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -318,7 +318,7 @@ let initial_goals p = Proofview.initial_goals p.entry let run_tactic env tac pr = let sp = pr.proofview in - let (_,tacticced_proofview,(status,(to_shelve,give_up))) = Proofview.apply env tac sp in + let (_,tacticced_proofview,(status,to_shelve,give_up)) = Proofview.apply env tac sp in let shelf = Proofview.in_proofview tacticced_proofview begin fun sigma -> let pre_shelf = pr.shelf@(Evd.future_goals sigma)@to_shelve in |