Fixed bugs #2001 (search_guard was overwriting the guard index given

by user) and #2017 (unification pattern test too crude leading to
regression wrt to 8.1).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11743 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 9 insertions, 6 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 6dad6471d7..62668f7f3e 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -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}
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index ad7c5e51ab..9a40ba319a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -80,7 +80,7 @@ val get_undo : unit -> int option
 
 val start_proof : 
   identifier -> goal_kind -> named_context_val -> constr ->
-    ?init_tac:tactic -> declaration_hook -> unit
+    ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit
 
 (* [restart_proof ()] restarts the current focused proof from the beginning
    or fails if no proof is focused *)
@@ -104,10 +104,11 @@ val suspend_proof : unit -> unit
 
 (*s [cook_proof opacity] turns the current proof (assumed completed) into
     a constant with its name, kind and possible hook (see [start_proof]);
-    it fails if there is no current proof of if it is not completed *)
+    it fails if there is no current proof of if it is not completed;
+    it also tells if the guardness condition has to be inferred. *)
 
 val cook_proof : (Refiner.pftreestate -> unit) -> 
-  identifier * (Entries.definition_entry * goal_kind * declaration_hook)
+  identifier * (Entries.definition_entry * bool * goal_kind * declaration_hook)
 
 (* To export completed proofs to xml *)
 val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit