diff options
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 77a884121e..25c8e2d802 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) @@ -1067,6 +1069,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 +1204,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 +1223,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 |