aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/interface/blast.ml6
-rw-r--r--pretyping/typeclasses.ml11
-rw-r--r--pretyping/typeclasses.mli2
-rw-r--r--tactics/class_tactics.ml49
-rw-r--r--tactics/eauto.ml410
-rw-r--r--tactics/eauto.mli2
-rw-r--r--theories/FSets/FMapFacts.v23
7 files changed, 31 insertions, 32 deletions
diff --git a/plugins/interface/blast.ml b/plugins/interface/blast.ml
index 57b4d1af8..2f0095a56 100644
--- a/plugins/interface/blast.ml
+++ b/plugins/interface/blast.ml
@@ -187,7 +187,7 @@ and e_my_find_search db_list local_db hdc concl =
match t with
| Res_pf (term,cl) -> unify_resolve st (term,cl)
| ERes_pf (term,cl) -> unify_e_resolve (term,cl)
- | Give_exact (c) -> e_give_exact_constr c
+ | Give_exact (c) -> e_give_exact c
| Res_pf_THEN_trivial_fail (term,cl) ->
tclTHEN (unify_e_resolve (term,cl))
(e_trivial_fail_db db_list local_db)
@@ -218,7 +218,7 @@ let e_possible_resolve db_list local_db gl =
(fst (head_constr_bound gl)) gl)
with Bound | Not_found -> []
-let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
+let assumption_tac_list id = apply_tac_list (e_give_exact (mkVar id))
let find_first_goal gls =
try first_goal gls with UserError _ -> assert false
@@ -266,7 +266,7 @@ module MySearchProblem = struct
let l =
filter_tactics s.tacres
(List.map
- (fun id -> (e_give_exact_constr (mkVar id),
+ (fun id -> (e_give_exact (mkVar id),
(str "Exact" ++ spc()++ pr_id id)))
(pf_ids_of_hyps g))
in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 219f9d127..2f2796f1c 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -315,17 +315,18 @@ let mark_unresolvables sigma =
Evd.add evs ev (mark_unresolvable evi))
sigma Evd.empty
-let rec is_class_type c =
+let rec is_class_type evd c =
match kind_of_term c with
- | Prod (_, _, t) -> is_class_type t
+ | Prod (_, _, t) -> is_class_type evd t
+ | Evar (e, _) when is_defined evd e -> is_class_type evd (Evarutil.nf_evar evd c)
| _ -> class_of_constr c <> None
-let is_class_evar evi =
- is_class_type evi.Evd.evar_concl
+let is_class_evar evd evi =
+ is_class_type evd evi.Evd.evar_concl
let has_typeclasses evd =
Evd.fold (fun ev evi has -> has ||
- (evi.evar_body = Evar_empty && is_class_evar evi && is_resolvable evi))
+ (evi.evar_body = Evar_empty && is_class_evar evd evi && is_resolvable evi))
evd false
let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 833cec6d5..d5f5d6182 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -80,7 +80,7 @@ val bool_out : Dyn.t -> bool
val is_resolvable : evar_info -> bool
val mark_unresolvable : evar_info -> evar_info
val mark_unresolvables : evar_map -> evar_map
-val is_class_evar : evar_info -> bool
+val is_class_evar : evar_map -> evar_info -> bool
val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool ->
env -> evar_defs -> evar_defs
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 2b9a48030..b163ed32a 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -91,7 +91,7 @@ open Auto
let e_give_exact flags c gl =
let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
if occur_existential t1 or occur_existential t2 then
- tclTHEN (Clenvtac.unify (* ~flags *) t1) (exact_no_check c) gl
+ tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl
else exact_check c gl
(* let t1 = (pf_type_of gl c) in *)
(* tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl *)
@@ -286,7 +286,8 @@ let hints_tac hints =
aux (succ i) tl)
in
let glsv = {it = list_map_i (fun j g -> g,
- { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp }) 1 gls; sigma = s}, fun _ -> v in
+ { info with auto_depth = j :: i :: info.auto_depth;
+ auto_last_tac = pp }) 1 gls; sigma = s}, fun _ -> v in
sk glsv fk
| [] -> fk ()
in aux 1 tacs }
@@ -477,8 +478,8 @@ let resolve_typeclass_evars d p env evd onlyargs split fail =
let pred =
if onlyargs then
(fun ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) &&
- Typeclasses.is_class_evar evi)
- else (fun ev evi -> Typeclasses.is_class_evar evi)
+ Typeclasses.is_class_evar evd evi)
+ else (fun ev evi -> Typeclasses.is_class_evar evd evi)
in resolve_all_evars d p env pred evd split fail
let solve_inst debug mode depth env evd onlyargs split fail =
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 09fc808c6..231483dc4 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -31,7 +31,7 @@ open Auto
open Rawterm
open Hiddentac
-let e_give_exact ?(flags=Unification.default_unify_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
+let e_give_exact ?(flags=auto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
if occur_existential t1 or occur_existential t2 then
tclTHEN (Clenvtac.unify ~flags t1) (exact_check c) gl
else exact_check c gl
@@ -49,10 +49,8 @@ TACTIC EXTEND eexact
| [ "eexact" constr(c) ] -> [ e_give_exact c ]
END
-let e_give_exact_constr = h_eexact
-
let registered_e_assumption gl =
- tclFIRST (List.map (fun id gl -> e_give_exact_constr (mkVar id) gl)
+ tclFIRST (List.map (fun id gl -> e_give_exact (mkVar id) gl)
(pf_ids_of_hyps gl)) gl
(************************************************************************)
@@ -137,7 +135,7 @@ and e_my_find_search_nodelta db_list local_db hdc concl =
match t with
| Res_pf (term,cl) -> unify_resolve_nodelta (term,cl)
| ERes_pf (term,cl) -> unify_e_resolve_nodelta (term,cl)
- | Give_exact (c) -> e_give_exact_constr c
+ | Give_exact (c) -> e_give_exact c
| Res_pf_THEN_trivial_fail (term,cl) ->
tclTHEN (unify_e_resolve_nodelta (term,cl))
(e_trivial_fail_db false db_list local_db)
@@ -267,7 +265,7 @@ module SearchProblem = struct
let l =
filter_tactics s.tacres
(List.map
- (fun id -> (e_give_exact_constr (mkVar id),
+ (fun id -> (e_give_exact (mkVar id),
(str "exact" ++ spc () ++ pr_id id)))
(pf_ids_of_hyps g))
in
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 1c6f9920f..d2ac36fe8 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -25,7 +25,7 @@ val e_assumption : tactic
val registered_e_assumption : tactic
-val e_give_exact_constr : constr -> tactic
+val e_give_exact : ?flags:Unification.unify_flags -> constr -> tactic
val gen_eauto : bool -> bool * int -> constr list ->
hint_db_name list option -> tactic
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 1ff9fbf20..cd80003a2 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -762,7 +762,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
Notation eqke := (@eq_key_elt elt).
Notation eqk := (@eq_key elt).
-
+
(** Complements about InA, NoDupA and findA *)
Lemma InA_eqke_eqk : forall k1 k2 e1 e2 l,
@@ -790,7 +790,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
intros. symmetry.
unfold eqb.
rewrite <- findA_NoDupA, InA_rev, findA_NoDupA
- by eauto using NoDupA_rev; eauto.
+ by eauto using NoDupA_rev; eauto. apply H0.
case_eq (findA (eqb k) (rev l)); auto.
intros e.
unfold eqb.
@@ -898,7 +898,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
intros k e a m' m'' H ? ? ?; eapply Hstep; eauto.
revert H; unfold l; rewrite InA_rev, elements_mapsto_iff; auto.
assert (Hdup : NoDupA eqk l).
- unfold l. apply NoDupA_rev; try red; eauto. apply elements_3w.
+ unfold l. apply NoDupA_rev; try red; unfold eq_key ; eauto.
+ apply elements_3w.
assert (Hsame : forall k, find k m = findA (eqb k) l).
intros k. unfold l. rewrite elements_o, findA_rev; auto.
apply elements_3w.
@@ -1106,8 +1107,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
intros (k,e) (k',e'); unfold eq_key; simpl; auto.
apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
- apply ForallList2_equiv1 with (eqA:=eqk); try red; eauto.
- apply NoDupA_rev; try red; eauto. apply elements_3w.
+ apply ForallList2_equiv1 with (eqA:=eqk); try red ; unfold eq_key ; eauto.
+ apply NoDupA_rev; try red ; unfold eq_key; eauto. apply elements_3w.
red; intros.
do 2 rewrite InA_rev.
destruct x; do 2 rewrite <- elements_mapsto_iff.
@@ -1139,7 +1140,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
unfold f'; intros (k1,e1) (k2,e2); unfold eq_key; simpl; auto.
apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
- apply ForallList2_equiv1 with (eqA:=eqk); try red; eauto.
+ apply ForallList2_equiv1 with (eqA:=eqk); try red; unfold eq_key ; eauto.
apply NoDupA_rev; try red; eauto. apply elements_3w.
rewrite InA_rev.
contradict H.
@@ -2163,8 +2164,7 @@ Module OrdProperties (M:S).
Qed.
Lemma fold_Add_Above : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
- (f:key->elt->A->A)(i:A),
- Proper (E.eq==>Leibniz==>eqA==>eqA) f ->
+ (f:key->elt->A->A)(i:A) (P:Proper (E.eq==>Leibniz==>eqA==>eqA) f),
Above x m1 -> Add x e m1 m2 ->
eqA (fold f m2 i) (f x e (fold f m1 i)).
Proof.
@@ -2172,7 +2172,7 @@ Module OrdProperties (M:S).
set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
transitivity (fold_right f' i (rev (elements m1 ++ (x,e)::nil))).
apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
- intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; unfold f'; simpl in *; apply H; auto.
+ intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; unfold f'; simpl in *. apply P; auto.
apply eqlistA_rev.
apply elements_Add_Above; auto.
rewrite distr_rev; simpl.
@@ -2180,8 +2180,7 @@ Module OrdProperties (M:S).
Qed.
Lemma fold_Add_Below : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
- (f:key->elt->A->A)(i:A),
- Proper (E.eq==>Leibniz==>eqA==>eqA) f ->
+ (f:key->elt->A->A)(i:A) (P:Proper (E.eq==>Leibniz==>eqA==>eqA) f),
Below x m1 -> Add x e m1 m2 ->
eqA (fold f m2 i) (fold f m1 (f x e i)).
Proof.
@@ -2189,7 +2188,7 @@ Module OrdProperties (M:S).
set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
transitivity (fold_right f' i (rev (((x,e)::nil)++elements m1))).
apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
- intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; unfold f'; simpl in *; apply H; auto.
+ intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; unfold f'; simpl in *; apply P; auto.
apply eqlistA_rev.
simpl; apply elements_Add_Below; auto.
rewrite distr_rev; simpl.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 13:50:18 +0000