diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 6d8f09ea..0aba9f5f 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pfedit.ml 10850 2008-04-25 18:07:44Z herbelin $ *) +(* $Id: pfedit.ml 11745 2009-01-04 18:43:08Z herbelin $ *) open Pp open Util @@ -34,6 +34,7 @@ open Safe_typing type proof_topstate = { mutable top_end_tac : tactic option; top_init_tac : tactic option; + top_compute_guard : bool; top_goal : goal; top_strength : Decl_kinds.goal_kind; top_hook : declaration_hook } @@ -207,7 +208,7 @@ let set_xml_cook_proof f = xml_cook_proof := f let cook_proof k = let (pfs,ts) = get_state() and ident = get_current_proof_name () in - let {evar_concl=concl} = ts.top_goal + let {evar_concl=concl} = ts.top_goal and strength = ts.top_strength in let pfterm = extract_pftreestate pfs in !xml_cook_proof (strength,pfs); @@ -217,7 +218,7 @@ let cook_proof k = const_entry_type = Some concl; const_entry_opaque = true; const_entry_boxed = false}, - strength, ts.top_hook)) + ts.top_compute_guard, strength, ts.top_hook)) let current_proof_statement () = let ts = get_topstate() in @@ -251,11 +252,12 @@ let set_end_tac tac = (* Modifying the current prooftree *) (*********************************************************************) -let start_proof na str sign concl ?init_tac hook = +let start_proof na str sign concl ?init_tac ?(compute_guard=false) hook = let top_goal = mk_goal sign concl None in let ts = { top_end_tac = None; top_init_tac = init_tac; + top_compute_guard = compute_guard; top_goal = top_goal; top_strength = str; top_hook = hook} |