- Fix bug in unification not taking into account the right meta

substitution. Makes unification succeed a bit more often, hence auto
works better in some cases.
- Backtrack the changes of auto using Hint Unfold to do more delta and add
a new tactic "new auto" which does that, for compatibility.

The first fix may have a big impact on the contribs, whereas the second
should make them compile again... we'll see.


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

9 files changed, 72 insertions, 65 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 90d6bb081..216900bdb 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -148,7 +148,7 @@ let expand_constant env flags c =
 let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n =
   let nb = nb_rel env in
   let trivial_unify pb (metasubst,_) m n =
-    match subst_defined_metas metas m with
+    match subst_defined_metas metasubst m with
     | Some m ->
 	(match flags.modulo_conv_on_closed_terms with
 	    Some flags ->
@@ -214,9 +214,9 @@ let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n =
 		  let pb = ConvUnderApp (len1,len2) in
 		  array_fold_left2 (unirec_rec curenv topconv true)
 		    (unirec_rec curenv pb true substn f1 f2) l1 l2
-		  with ex when precatchable_exception ex ->
-		    expand curenv pb b substn cM f1 l1 cN f2 l2)
-
+		with ex when precatchable_exception ex ->
+		  expand curenv pb b substn cM f1 l1 cN f2 l2)
+		
 	| _ -> 
 	    let (f1,l1) = 
 	      match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 8823efe0b..111245e11 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -637,34 +637,37 @@ let conclPattern concl pat tac gl =
 (* Papageno : cette fonction a été pas mal simplifiée depuis que la base
   de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
 
-let transparent_state_union (xids, xcsts) (yids, ycsts) = 
-  (Idpred.union xids yids, Cpred.union xcsts ycsts)
-
-let rec trivial_fail_db db_list local_db gl =
+let rec trivial_fail_db mod_delta db_list local_db gl =
   let intro_tac = 
     tclTHEN intro 
       (fun g'->
 	 let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
-	 in trivial_fail_db db_list (add_hint_list hintl local_db) g')
+	 in trivial_fail_db mod_delta db_list (add_hint_list hintl local_db) g')
   in
   tclFIRST 
     (assumption::intro_tac::
      (List.map tclCOMPLETE 
-	(trivial_resolve db_list local_db (pf_concl gl)))) gl
+       (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl
 
-and my_find_search db_list local_db hdc concl =
+and my_find_search mod_delta db_list local_db hdc concl =
   let tacl = 
     if occur_existential concl then 
       list_map_append
 	(fun (st, db) -> 
-	  List.map (fun x -> (st,x)) (Hint_db.map_all hdc db))
+	  let st = if mod_delta then st else empty_transparent_state in
+	    List.map (fun x -> (st,x)) (Hint_db.map_all hdc db))
 	(local_db::db_list)
-    else 
+    else
       list_map_append (fun ((ids, csts as st), db) -> 
-	let l = 
-(* 	  if Idpred.is_empty ids && Cpred.is_empty csts *)
-(* 	  then  *)Hint_db.map_auto (hdc,concl) db
-(* 	  else Hint_db.map_all hdc db *)
+	let st, l = 
+	  if not mod_delta then
+	    empty_transparent_state, Hint_db.map_auto (hdc,concl) db
+	  else 
+	    let l =
+	      if (Idpred.is_empty ids && Cpred.is_empty csts)
+	      then Hint_db.map_auto (hdc,concl) db
+	      else Hint_db.map_all hdc db
+	    in st, l
 	in List.map (fun x -> (st,x)) l)
       	(local_db::db_list)
   in
@@ -678,17 +681,17 @@ and my_find_search db_list local_db hdc concl =
 	  | Res_pf_THEN_trivial_fail (term,cl) -> 
 	      tclTHEN 
 		(unify_resolve st (term,cl)) 
-		(trivial_fail_db db_list local_db)
+		(trivial_fail_db mod_delta db_list local_db)
 	  | Unfold_nth c -> unfold_in_concl [[],c]
 	  | Extern tacast -> 
 	      conclPattern concl (Option.get p) tacast))
     tacl
 
-and trivial_resolve db_list local_db cl = 
+and trivial_resolve mod_delta db_list local_db cl = 
   try 
     let hdconstr = List.hd (head_constr_bound cl []) in
     priority 
-      (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
+      (my_find_search mod_delta db_list local_db (head_of_constr_reference hdconstr) cl)
   with Bound | Not_found -> 
     []
 
@@ -702,13 +705,13 @@ let trivial lems dbnames gl =
 	   error ("trivial: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
-  tclTRY (trivial_fail_db db_list (make_local_hint_db false lems gl)) gl 
+  tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl 
     
 let full_trivial lems gl =
   let dbnames = Hintdbmap.dom !searchtable in
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
-  tclTRY (trivial_fail_db db_list (make_local_hint_db false lems gl)) gl
+  tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl
 
 let gen_trivial lems = function
   | None -> full_trivial lems
@@ -724,11 +727,11 @@ let h_trivial lems l =
 (*                       The classical Auto tactic                        *)
 (**************************************************************************)
 
-let possible_resolve db_list local_db cl =
+let possible_resolve mod_delta db_list local_db cl =
   try 
     let hdconstr = List.hd (head_constr_bound cl []) in
     List.map snd 
-      (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
+      (my_find_search mod_delta db_list local_db (head_of_constr_reference hdconstr) cl)
   with Bound | Not_found -> 
     []
 
@@ -754,7 +757,7 @@ let decomp_empty_term c gls =
 (* n is the max depth of search *)
 (* local_db contains the local Hypotheses *)
 
-let rec search_gen decomp n db_list local_db extra_sign goal =
+let rec search_gen decomp n mod_delta db_list local_db extra_sign goal =
   if n=0 then error "BOUND 2";
   let decomp_tacs = match decomp with 
     | 0 -> [] 
@@ -765,7 +768,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	   (fun id -> tclTHENSEQ
                [decomp_unary_term (mkVar id);
                 clear [id];
-		search_gen decomp p db_list local_db []])
+		search_gen decomp p mod_delta db_list local_db []])
 	   (pf_ids_of_hyps goal)) 
   in
   let intro_tac = 
@@ -779,14 +782,14 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 		(mkVar hid, htyp)]
 	   with Failure _ -> [] 
 	 in
-         search_gen decomp n db_list (add_hint_list hintl local_db) [d] g') 
+         search_gen decomp n mod_delta db_list (add_hint_list hintl local_db) [d] g') 
   in
   let rec_tacs = 
     List.map 
       (fun ntac -> 
 	 tclTHEN ntac
-	   (search_gen decomp (n-1) db_list local_db empty_named_context))
-      (possible_resolve db_list local_db (pf_concl goal))
+	   (search_gen decomp (n-1) mod_delta db_list local_db empty_named_context))
+      (possible_resolve mod_delta db_list local_db (pf_concl goal))
   in 
   tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal
 
@@ -795,7 +798,7 @@ let search = search_gen 0
 
 let default_search_depth = ref 5
 
-let auto n lems dbnames gl =
+let delta_auto mod_delta n lems dbnames gl =
   let db_list = 
     List.map
       (fun x -> 
@@ -806,17 +809,24 @@ let auto n lems dbnames gl =
       ("core"::dbnames) 
   in
   let hyps = pf_hyps gl in
-  tclTRY (search n db_list (make_local_hint_db false lems gl) hyps) gl
+  tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl) hyps) gl
+
+let auto = delta_auto false
+
+let new_auto = delta_auto true
 
 let default_auto = auto !default_search_depth [] []
 
-let full_auto n lems gl = 
+let delta_full_auto mod_delta n lems gl = 
   let dbnames = Hintdbmap.dom !searchtable in
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
   let hyps = pf_hyps gl in
-  tclTRY (search n db_list (make_local_hint_db false lems gl) hyps) gl
-  
+  tclTRY (search n false db_list (make_local_hint_db false lems gl) hyps) gl
+
+let full_auto = delta_full_auto false
+let new_full_auto = delta_full_auto true
+
 let default_full_auto gl = full_auto !default_search_depth [] gl
 
 let gen_auto n lems dbnames =
@@ -843,7 +853,7 @@ let default_search_decomp = ref 1
 
 let destruct_auto des_opt lems n gl = 
   let hyps = pf_hyps gl in
-  search_gen des_opt n (List.map searchtable_map ["core";"extcore"])
+  search_gen des_opt n false (List.map searchtable_map ["core";"extcore"])
     (make_local_hint_db false lems gl) hyps gl
     
 let dautomatic des_opt lems n = tclTRY (destruct_auto des_opt lems n)
@@ -918,7 +928,7 @@ let rec super_search n db_list local_db argl goal =
          (fun ntac -> 
             tclTHEN ntac 
               (super_search (n-1) db_list local_db argl))
-         (possible_resolve db_list local_db (pf_concl goal)))
+         (possible_resolve false db_list local_db (pf_concl goal)))
       @
       (compileAutoArgList  
          (super_search (n-1) db_list local_db argl) argl))) goal
diff --git a/tactics/auto.mli b/tactics/auto.mli
index bb22b6c81..91f4182fa 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -152,12 +152,20 @@ val conclPattern : constr -> constr_pattern -> Tacexpr.glob_tactic_expr -> tacti
 
 val auto : int -> constr list -> hint_db_name list -> tactic
 
+(* Auto with more delta. *)
+
+val new_auto : int -> constr list -> hint_db_name list -> tactic
+
 (* auto with default search depth and with the hint database "core" *)
 val default_auto : tactic
 
 (* auto with all hint databases except the "v62" compatibility database *)
 val full_auto : int -> constr list -> tactic
 
+(* auto with all hint databases except the "v62" compatibility database
+   and doing delta *)
+val new_full_auto : int -> constr list -> tactic
+
 (* auto with default search depth and with all hint databases 
    except the "v62" compatibility database *)
 val default_full_auto : tactic
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 03b29d523..62d137b7a 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -373,6 +373,15 @@ TACTIC EXTEND eauto
     [ gen_eauto false (make_dimension n p) lems db ]
 END
 
+TACTIC EXTEND new_eauto
+| [ "new" "auto" int_or_var_opt(n) auto_using(lems) 
+    hintbases(db) ] ->
+    [ match db with
+      | None -> new_full_auto (make_depth n) lems
+      | Some l ->
+	  new_auto (make_depth n) lems l ]
+END
+      
 TACTIC EXTEND debug_eauto
 | [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) 
     hintbases(db) ] ->
diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v
index ab7b4a254..5cc8f0284 100644
--- a/theories/Ints/num/NMake.v
+++ b/theories/Ints/num/NMake.v
@@ -5177,9 +5177,6 @@ Qed.
    rewrite H1; simpl Z_of_nat; change (2^1) with (2).
    unfold base.
    apply Zpower_le_monotone; split; auto with zarith.
-   rewrite Zmult_comm; repeat rewrite <- Zmult_assoc.
-     repeat rewrite <- Zpos_xO.
-   refine (Zle_refl _).
  intros n; case n; clear n.
  intros H1; rewrite spec_reduce_2; unfold to_Z.
  apply (znz_of_pos_correct w2_spec).
@@ -5187,19 +5184,13 @@ Qed.
    rewrite H1; simpl Z_of_nat; change (2^2) with (2 * 2).
    unfold base.
    apply Zpower_le_monotone; split; auto with zarith.
-   rewrite Zmult_comm; repeat rewrite <- Zmult_assoc.
-     repeat rewrite <- Zpos_xO.
-   refine (Zle_refl _).
  intros n; case n; clear n.
  intros H1; rewrite spec_reduce_3; unfold to_Z.
  apply (znz_of_pos_correct w3_spec).
  apply Zlt_le_trans with (1 := pheight_correct x).
    rewrite H1; simpl Z_of_nat; change (2^3) with (2 * 2 * 2).
    unfold base.
-   apply Zpower_le_monotone; split; auto with zarith.
-   rewrite Zmult_comm; repeat rewrite <- Zmult_assoc.
-     repeat rewrite <- Zpos_xO.
-   refine (Zle_refl _).
+   apply Zpower_le_monotone; split; auto with zarith. 
  intros n; case n; clear n.
  intros H1; rewrite spec_reduce_4; unfold to_Z.
  apply (znz_of_pos_correct w4_spec).
@@ -5207,9 +5198,6 @@ Qed.
    rewrite H1; simpl Z_of_nat; change (2^4) with (2 * 2 * 2 * 2).
    unfold base.
    apply Zpower_le_monotone; split; auto with zarith.
-   rewrite Zmult_comm; repeat rewrite <- Zmult_assoc.
-     repeat rewrite <- Zpos_xO.
-   refine (Zle_refl _).
  intros n; case n; clear n.
  intros H1; rewrite spec_reduce_5; unfold to_Z.
  apply (znz_of_pos_correct w5_spec).
@@ -5217,9 +5205,6 @@ Qed.
    rewrite H1; simpl Z_of_nat; change (2^5) with (2 * 2 * 2 * 2 * 2).
    unfold base.
    apply Zpower_le_monotone; split; auto with zarith.
-   rewrite Zmult_comm; repeat rewrite <- Zmult_assoc.
-     repeat rewrite <- Zpos_xO.
-   refine (Zle_refl _).
  intros n; case n; clear n.
  intros H1; rewrite spec_reduce_6; unfold to_Z.
  apply (znz_of_pos_correct w6_spec).
@@ -5227,9 +5212,6 @@ Qed.
    rewrite H1; simpl Z_of_nat; change (2^6) with (2 * 2 * 2 * 2 * 2 * 2).
    unfold base.
    apply Zpower_le_monotone; split; auto with zarith.
-   rewrite Zmult_comm; repeat rewrite <- Zmult_assoc.
-     repeat rewrite <- Zpos_xO.
-   refine (Zle_refl _).
  intros n.
  intros H1; rewrite spec_reduce_n; unfold to_Z.
  simpl minus; rewrite <- minus_n_O.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 5ab27cfc7..78a2db534 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -686,8 +686,7 @@ Section ListOps.
     rewrite app_nth1; auto.
     rewrite (minus_plus_simpl_l_reverse (length l) n 1).
     replace (1 + length l) with (S (length l)); auto with arith.
-    rewrite <- minus_Sn_m; auto with arith; simpl.
-    apply IHl; auto.
+    rewrite <- minus_Sn_m; auto with arith.
     rewrite rev_length; auto.
   Qed.
 
@@ -1363,7 +1362,6 @@ End Fold_Right_Recursor.
       destruct n; destruct d; simpl; auto.
       destruct a; destruct (split l); simpl; auto.
       destruct a; destruct (split l); simpl in *; auto.
-      rewrite IHl; simpl; auto.
     Qed.
 
     Lemma split_length_l : forall (l:list (A*B)),
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index ac3664054..8116045b6 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -101,6 +101,7 @@ Section Sets_as_an_algebra.
     intros X x H'; red in |- *.
     intros x0 H'0; try assumption.
     elim (classic (x = x0)); intro K; auto with sets.
+    elim K; auto with sets.
   Qed.
   
   Lemma add_soustr_1 :
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 4057ba022..6826e0c51 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -110,8 +110,8 @@ Proof.
 intros s1; elim s1; simpl in |- *; auto.
 intros s2 n; rewrite plus_comm; simpl in |- *; auto.
 intros a s1' Rec s2 n; case n; simpl in |- *; auto.
-generalize (Rec s2 0); simpl in |- *; auto.
-intros n0; rewrite <- Plus.plus_Snm_nSm; auto.
+generalize (Rec s2 0); simpl in |- *; auto. intros.
+rewrite <- Plus.plus_Snm_nSm; auto.
 Qed.
 
 (** *** Substrings *)
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index b862d663b..9524bd44f 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -171,12 +171,11 @@ Qed.
 Theorem Zpower_ge_0: forall x y, 0 <= x -> 0 <= x^y. 
 Proof.
   intros x y; case y; auto with zarith.
-  simpl; auto with zarith.
   intros p H1; assert (H: 0 <= Zpos p); auto with zarith.
-  generalize H; pattern (Zpos p); apply natlike_ind; auto.
-  intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith.
-  apply Zmult_le_0_compat; auto with zarith.
-  generalize H1; case x; compute; intros; auto; discriminate.
+  generalize H; pattern (Zpos p); apply natlike_ind; auto with zarith.
+  intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith. 
+  apply Zmult_le_0_compat; auto with zarith.  
+  generalize H1; case x; compute; intros; auto; try discriminate.
 Qed.
 
 Theorem Zpower_le_monotone2: