diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 2 | ||||
| -rw-r--r-- | proofs/proofview.mli | 9 |
2 files changed, 10 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 6e653806b7..64ea5aea01 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -887,7 +887,7 @@ module Unsafe = struct end - +module UnsafeRepr = Proof.Unsafe (** {7 Notations} *) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 5a9e7f39f0..98e1477ff1 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -405,6 +405,15 @@ module Unsafe : sig val mark_as_goal : proofview -> Evar.t -> proofview end +(** This module gives access to the innards of the monad. Its use is + restricted to very specific cases. *) +module UnsafeRepr : +sig + type state = Proofview_monad.Logical.Unsafe.state + val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t + val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic +end + (** {7 Notations} *) module Notations : sig |