diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-05 13:15:15 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-05 13:15:15 +0100 |
commit | 736e86e06b5831a0dd4b6a655708b4ffd2b4ee64 (patch) | |
tree | f1f572e011f0e5e476256d58517258774bdf149e /engine/proofview.ml | |
parent | a46a04577e34c69b42c2728ec1e0babb5be23e31 (diff) | |
parent | 7267e31fa4456aee62a1e39dfdb7e38a8832f93f (diff) |
Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad
Diffstat (limited to 'engine/proofview.ml')
-rw-r--r-- | engine/proofview.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 77a884121..0924b7a02 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1067,6 +1067,9 @@ module Goal = struct } let assume (gl : t) = (gl : t) + + let print { sigma; self } = { Evd.it = self; sigma } + let state { state=state } = state let env {env} = env @@ -1199,7 +1202,7 @@ let tclCHECKINTERRUPT = module V82 = struct type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - let tactic tac = + let tactic ?(nf_evars=true) tac = (* spiwack: we ignore the dependencies between goals here, expectingly preserving the semantics of <= 8.2 tactics *) (* spiwack: convenience notations, waiting for ocaml 3.12 *) @@ -1218,7 +1221,7 @@ module V82 = struct let (initgoals_w_state, initevd) = Evd.Monad.List.map (fun g_w_s s -> let g, w = drop_state g_w_s, get_state g_w_s in - let g, s = goal_nf_evar s g in + let g, s = if nf_evars then goal_nf_evar s g else g, s in goal_with_state g w, s) ps.comb ps.solution in let (goalss,evd) = Evd.Monad.List.map tac initgoals_w_state initevd in |