diff options
| author | Pierre-Marie Pédrot | 2014-11-21 19:28:46 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-11-22 13:23:28 +0100 |
| commit | 34921bb2391e8ce8b0fa00c300d218d2ef6f27e2 (patch) | |
| tree | 0ac55299bfc367aa55ffebf4cef0d3edbe5fd50b /proofs/logic_monad.mli | |
| parent | 228a39aab291af446b9419673c05d224dfbd8a72 (diff) | |
Exporting a primitive allowing to run completely the tactic monad.
Diffstat (limited to 'proofs/logic_monad.mli')
| -rw-r--r-- | proofs/logic_monad.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli index a36b017fb0..46cab18d25 100644 --- a/proofs/logic_monad.mli +++ b/proofs/logic_monad.mli @@ -148,5 +148,10 @@ module Logical (P:Param) : sig val lift : 'a NonLogical.t -> 'a t - val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) NonLogical.t + type 'a reified + + val repr : 'a reified -> ('a, exn -> 'a reified) list_view NonLogical.t + + val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) reified + end |