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 | |
| parent | f02f64a21863ce03f2da4ff04cd003051f96801f (diff) | |
Removing the evar_map argument from s_enter.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 10 | ||||
| -rw-r--r-- | proofs/proofview.mli | 4 |
2 files changed, 6 insertions, 8 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index bded518e78..96ba88233e 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -978,7 +978,7 @@ module Goal = struct end 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 } let s_enter f = InfoL.tag (Info.Dispatch) begin @@ -987,8 +987,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try let gl = gmake env sigma goal in - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (tac, sigma, _) = f.s_enter gl sigma in + let Sigma (tac, sigma, _) = f.s_enter gl in let sigma = Sigma.to_evar_map sigma in tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) with e when catchable_exception e -> @@ -1004,8 +1003,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try let (gl, sigma) = nf_gmake env sigma goal in - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (tac, sigma, _) = f.s_enter gl sigma in + let Sigma (tac, sigma, _) = f.s_enter gl in let sigma = Sigma.to_evar_map sigma in tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) with e when catchable_exception e -> @@ -1263,5 +1261,5 @@ module Notations = struct 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 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 |