Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

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}