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.ml | |
| parent | f02f64a21863ce03f2da4ff04cd003051f96801f (diff) | |
Removing the evar_map argument from s_enter.
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 10 |
1 files changed, 4 insertions, 6 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 |