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/proofview.mli | |
| 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/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index d822f933b..45a0c9484 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -133,7 +133,7 @@ type 'a case = case it is [false]. *) val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview - * (bool*(Goal.goal list*Goal.goal list)) + * (bool*Goal.goal list*Goal.goal list) (*** tacticals ***) |