diff options
| author | Pierre-Marie Pédrot | 2015-10-29 19:14:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-29 19:22:59 +0100 |
| commit | 250df8586a776eaadc3553b5ceef98d3696fffdb (patch) | |
| tree | 2e86418dead74cc799f2838b43c8f602dc70cad3 /proofs/proofview.mli | |
| parent | f02f64a21863ce03f2da4ff04cd003051f96801f (diff) | |
Removing the evar_map argument from s_enter.
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index aafd4c5759..66603b9764 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -464,7 +464,7 @@ module Goal : sig val enter : ([ `LZ ], unit tactic) enter -> unit tactic type ('a, 'b) s_enter = - { s_enter : 'r. ('a, 'r) t -> 'r Sigma.t -> ('b, 'r) Sigma.sigma } + { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } (** A variant of {!enter} allows to work with a monotonic state. The evarmap returned by the argument is put back into the current state before firing @@ -608,5 +608,5 @@ module Notations : sig type ('a, 'b) enter = ('a, 'b) Goal.enter = { enter : 'r. ('a, 'r) Goal.t -> 'b } type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter = - { s_enter : 'r. ('a, 'r) Goal.t -> 'r Sigma.t -> ('b, 'r) Sigma.sigma } + { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma } end |