diff options
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index 764a4a0058..8ec53ac78c 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -145,7 +145,7 @@ val unfocus : focus_context -> proofview -> proofview (** The abstract type of tactics *) -type +'a tactic +type +'a tactic (** Applies a tactic to the current proofview. Returns a tuple [a,pv,(b,sh,gu)] where [a] is the return value of the tactic, [pv] @@ -170,7 +170,7 @@ val apply (** Unit of the tactic monad. *) val tclUNIT : 'a -> 'a tactic - + (** Bind operation of the tactic monad. *) val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic @@ -440,7 +440,7 @@ module Unsafe : sig goal. If goals have been solved in [sigma] they will still appear as unsolved goals. *) val tclEVARS : Evd.evar_map -> unit tactic - + (** Like {!tclEVARS} but also checks whether goals have been solved. *) val tclEVARSADVANCE : Evd.evar_map -> unit tactic |