aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/blast.ml15
-rw-r--r--pretyping/unification.ml3
-rw-r--r--tactics/auto.ml18
-rw-r--r--tactics/auto.mli4
-rw-r--r--tactics/eauto.ml417
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1784.v2
-rw-r--r--theories/Ints/num/NMake.v6
-rw-r--r--theories/Lists/List.v2
-rw-r--r--theories/ZArith/Zpow_facts.v1
9 files changed, 49 insertions, 19 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 4df6108b6..10fafaefc 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -168,11 +168,14 @@ let rec e_trivial_fail_db db_list local_db goal =
and e_my_find_search db_list local_db hdc concl =
let hdc = head_of_constr_reference hdc in
+ let flags = Auto.auto_unif_flags in
let hintl =
if occur_existential concl then
- list_map_append (fun (st, db) -> List.map (fun x -> (st, x)) (Hint_db.map_all hdc db)) (local_db::db_list)
+ list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x))
+ (Hint_db.map_all hdc db)) (local_db::db_list)
else
- list_map_append (fun (st, db) -> List.map (fun x -> (st, x)) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+ list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x))
+ (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
in
let tac_of_hint =
fun (st, ({pri=b; pat = p; code=t} as _patac)) ->
@@ -380,12 +383,14 @@ let rec trivial_fail_db db_list local_db gl =
(trivial_resolve db_list local_db (pf_concl gl)))) gl
and my_find_search db_list local_db hdc concl =
+ let flags = Auto.auto_unif_flags in
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)) (local_db::db_list)
+ list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x)
+ (Hint_db.map_all hdc db)) (local_db::db_list)
else
- list_map_append (fun (st, db) -> List.map (fun x -> st, x) (Hint_db.map_auto (hdc,concl) db))
- (local_db::db_list)
+ list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x)
+ (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
in
List.map
(fun (st, {pri=b; pat=p; code=t} as _patac) ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 578afdb75..1063342e5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -145,7 +145,8 @@ let expand_constant env flags c =
let unify_0_with_initial_metas subst 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 metasubst m with
+ let subst = if flags.use_metas_eagerly then metasubst else fst subst in
+ match subst_defined_metas subst m with
| Some m ->
(match flags.modulo_conv_on_closed_terms with
Some flags ->
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0b1f29dc3..816bd61ca 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -591,9 +591,9 @@ let auto_unif_flags = {
(* Try unification with the precompiled clause, then use registered Apply *)
-let unify_resolve st (c,clenv) gls =
+let unify_resolve flags (c,clenv) gls =
let clenv' = connect_clenv gls clenv in
- let _ = clenv_unique_resolver false ~flags:{auto_unif_flags with modulo_delta = st} clenv' gls in
+ let _ = clenv_unique_resolver false ~flags clenv' gls in
h_apply true false (c,NoBindings) gls
(* builds a hint database from a constr signature *)
@@ -649,24 +649,32 @@ let rec trivial_fail_db mod_delta db_list local_db gl =
(trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl
and my_find_search mod_delta db_list local_db hdc concl =
+ let flags =
+ if mod_delta then {auto_unif_flags with use_metas_eagerly = true}
+ else auto_unif_flags
+ in
let tacl =
if occur_existential concl then
list_map_append
(fun (st, db) ->
- let st = if mod_delta then st else empty_transparent_state in
+ let st =
+ if mod_delta then
+ {flags with modulo_delta = st}
+ else flags
+ in
List.map (fun x -> (st,x)) (Hint_db.map_all hdc db))
(local_db::db_list)
else
list_map_append (fun ((ids, csts as st), db) ->
let st, l =
if not mod_delta then
- empty_transparent_state, Hint_db.map_auto (hdc,concl) db
+ flags, 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 {flags with modulo_delta = st}, l
in List.map (fun x -> (st,x)) l)
(local_db::db_list)
in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 91f4182fa..7853235be 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -138,8 +138,10 @@ val priority : (int * 'a) list -> 'a list
val default_search_depth : int ref
+val auto_unif_flags : Unification.unify_flags
+
(* Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve : transparent_state -> (constr * clausenv) -> tactic
+val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic
(* [ConclPattern concl pat tacast]:
if the term concl matches the pattern pat, (in sense of
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 62d137b7a..3894dfd1f 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -85,14 +85,15 @@ TACTIC EXTEND prolog
END
open Auto
+open Unification
(***************************************************************************)
(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
(***************************************************************************)
-let unify_e_resolve (c,clenv) gls =
+let unify_e_resolve flags (c,clenv) gls =
let clenv' = connect_clenv gls clenv in
- let _ = clenv_unique_resolver false clenv' gls in
+ let _ = clenv_unique_resolver false ~flags clenv' gls in
h_simplest_eapply c gls
let rec e_trivial_fail_db db_list local_db goal =
@@ -112,9 +113,13 @@ and e_my_find_search db_list local_db hdc concl =
let hdc = head_of_constr_reference hdc in
let hintl =
if occur_existential concl then
- list_map_append (fun (st, db) -> List.map (fun x -> st, x) (Hint_db.map_all hdc db)) (local_db::db_list)
+ list_map_append (fun (st, db) ->
+ let flags = {auto_unif_flags with modulo_delta = st} in
+ List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
else
- list_map_append (fun (st, db) -> List.map (fun x -> st, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+ list_map_append (fun (st, db) ->
+ let flags = {auto_unif_flags with modulo_delta = st} in
+ List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
in
let tac_of_hint =
fun (st, {pri=b; pat = p; code=t}) ->
@@ -122,10 +127,10 @@ and e_my_find_search db_list local_db hdc concl =
let tac =
match t with
| Res_pf (term,cl) -> unify_resolve st (term,cl)
- | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
+ | ERes_pf (term,cl) -> unify_e_resolve st (term,cl)
| Give_exact (c) -> e_give_exact_constr c
| Res_pf_THEN_trivial_fail (term,cl) ->
- tclTHEN (unify_e_resolve (term,cl))
+ tclTHEN (unify_e_resolve st (term,cl))
(e_trivial_fail_db db_list local_db)
| Unfold_nth c -> unfold_in_concl [[],c]
| Extern tacast -> conclPattern concl
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index d6b7660b2..616dd26f5 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -85,7 +85,7 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
end
end.
-Next Obligation. apply H; inversion H0; subst; trivial. reflexivity. Defined.
+Next Obligation. apply H; inversion H0; subst; trivial. Defined.
Next Obligation. inversion H. Defined.
Next Obligation. inversion H. Defined.
Next Obligation. inversion H; subst. Defined.
diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v
index c857da385..8cb779350 100644
--- a/theories/Ints/num/NMake.v
+++ b/theories/Ints/num/NMake.v
@@ -5182,6 +5182,7 @@ Qed.
rewrite H1; simpl Z_of_nat; change (2^1) with (2).
unfold base.
apply Zpower_le_monotone; split; auto with zarith.
+ apply Zeq_le; apply Zmult_comm.
intros n; case n; clear n.
intros H1; rewrite spec_reduce_2; unfold to_Z.
apply (znz_of_pos_correct w2_spec).
@@ -5189,6 +5190,7 @@ Qed.
rewrite H1; simpl Z_of_nat; change (2^2) with (2 * 2).
unfold base.
apply Zpower_le_monotone; split; auto with zarith.
+ apply Zeq_le; apply Zmult_comm.
intros n; case n; clear n.
intros H1; rewrite spec_reduce_3; unfold to_Z.
apply (znz_of_pos_correct w3_spec).
@@ -5196,6 +5198,7 @@ Qed.
rewrite H1; simpl Z_of_nat; change (2^3) with (2 * 2 * 2).
unfold base.
apply Zpower_le_monotone; split; auto with zarith.
+ apply Zeq_le; apply Zmult_comm.
intros n; case n; clear n.
intros H1; rewrite spec_reduce_4; unfold to_Z.
apply (znz_of_pos_correct w4_spec).
@@ -5203,6 +5206,7 @@ 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.
+ apply Zeq_le; apply Zmult_comm.
intros n; case n; clear n.
intros H1; rewrite spec_reduce_5; unfold to_Z.
apply (znz_of_pos_correct w5_spec).
@@ -5210,6 +5214,7 @@ 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.
+ apply Zeq_le; apply Zmult_comm.
intros n; case n; clear n.
intros H1; rewrite spec_reduce_6; unfold to_Z.
apply (znz_of_pos_correct w6_spec).
@@ -5217,6 +5222,7 @@ 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.
+ apply Zeq_le; apply Zmult_comm.
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 78a2db534..51d3f192d 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -687,6 +687,7 @@ Section ListOps.
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.
+ apply IHl ; auto with arith.
rewrite rev_length; auto.
Qed.
@@ -1362,6 +1363,7 @@ 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.
+ apply IHl.
Qed.
Lemma split_length_l : forall (l:list (A*B)),
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index 9524bd44f..8f86fdf79 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -171,6 +171,7 @@ 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 with zarith.
intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 10:19:37 +0000