diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-24 15:11:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-24 15:13:12 +0200 |
| commit | ae5ea0c9d5c0e9a39a50a2348b2b8f08938d5f5c (patch) | |
| tree | 2ba9b3c26e3627fe70bf095bdf650c8d375e9176 /proofs/proofview_monad.mli | |
| parent | fb4187a6d475719bada0a7fe1b7902a36e06d658 (diff) | |
Adding a tail-rec tclONCE.
Diffstat (limited to 'proofs/proofview_monad.mli')
| -rw-r--r-- | proofs/proofview_monad.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli index 4d4e4470c..7a86c7969 100644 --- a/proofs/proofview_monad.mli +++ b/proofs/proofview_monad.mli @@ -65,6 +65,7 @@ module Logical : sig val zero : exn -> 'a t val plus : 'a t -> (exn -> 'a t) -> 'a t val split : 'a t -> (('a,(exn->'a t)) list_view) t + val once : 'a t -> 'a t val lift : 'a NonLogical.t -> 'a t |