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, 12 insertions, 12 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 07f501956..1273d43fe 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -343,11 +343,11 @@ let (inDec,outDec) =
 let start_hook = ref ignore
 let set_start_hook = (:=) start_hook
 
-let start_proof id kind c ?init_tac hook =
+let start_proof id kind c ?init_tac ?(compute_guard=false) hook =
   let sign = Global.named_context () in
   let sign = clear_proofs sign in
   !start_hook c;
-  Pfedit.start_proof id kind sign c ?init_tac:init_tac hook
+  Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook
 
 let adjust_guardness_conditions const =
   (* Try all combinations... not optimal *)
@@ -361,8 +361,8 @@ let adjust_guardness_conditions const =
       { const with const_entry_body = mkFix ((indexes,0),fixdecls) }
   | c -> const
 
-let save id const (locality,kind) hook =
-  let const = adjust_guardness_conditions const in
+let save id const do_guard (locality,kind) hook =
+  let const = if do_guard then adjust_guardness_conditions const else const in
   let {const_entry_body = pft;
        const_entry_type = tpo;
        const_entry_opaque = opacity } = const in
@@ -383,9 +383,9 @@ let save_hook = ref ignore
 let set_save_hook f = save_hook := f
 
 let save_named opacity =
-  let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in
+  let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
   let const = { const with const_entry_opaque = opacity } in
-  save id const persistence hook
+  save id const do_guard persistence hook
 
 let make_eq_decidability ind = 
     (* fetching data *)
@@ -1220,7 +1220,7 @@ let start_proof_com kind thms hook =
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
 	  hook strength ref) thms_data in
-      start_proof id kind t ?init_tac:rec_tac hook
+      start_proof id kind t ?init_tac:rec_tac ~compute_guard:true hook
 
 let check_anonymity id save_ident =
   if atompart_of_id id <> "Unnamed_thm" then
@@ -1230,17 +1230,17 @@ let check_anonymity id save_ident =
 *)
 
 let save_anonymous opacity save_ident =
-  let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in
+  let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
   let const = { const with const_entry_opaque = opacity } in
   check_anonymity id save_ident;
-  save save_ident const persistence hook
+  save save_ident const do_guard persistence hook
 
 let save_anonymous_with_strength kind opacity save_ident =
-  let id,(const,_,hook) = Pfedit.cook_proof !save_hook in
+  let id,(const,do_guard,_,hook) = Pfedit.cook_proof !save_hook in
   let const = { const with const_entry_opaque = opacity } in
   check_anonymity id save_ident;
   (* we consider that non opaque behaves as local for discharge *)
-  save save_ident const (Global, Proof kind) hook
+  save save_ident const do_guard (Global, Proof kind) hook
 
 let admit () =
   let (id,k,typ,hook) = Pfedit.current_proof_statement () in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 8ccaaed35..7cf088901 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -109,7 +109,7 @@ val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 val set_start_hook : (types -> unit) -> unit
 
 val start_proof : identifier -> goal_kind -> types ->
-  ?init_tac:Proof_type.tactic -> declaration_hook -> unit
+  ?init_tac:Proof_type.tactic -> ?compute_guard:bool -> declaration_hook -> unit
 
 val start_proof_com : goal_kind -> 
   (lident option * (local_binder list * constr_expr)) list ->