summaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml48
-rw-r--r--tactics/equality.ml28
-rw-r--r--tactics/tacinterp.ml4
3 files changed, 27 insertions, 13 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index d05ae680..3a980ef9 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -276,7 +276,7 @@ let make_hints g st only_classes sign =
(PathEmpty, []) sign
in Hint_db.add_list hintlist (Hint_db.empty st true)
-let autogoal_hints_cache : (Environ.named_context_val * hint_db) option ref = ref None
+let autogoal_hints_cache : (bool * Environ.named_context_val * hint_db) option ref = ref None
let freeze () = !autogoal_hints_cache
let unfreeze v = autogoal_hints_cache := v
let init () = autogoal_hints_cache := None
@@ -293,9 +293,11 @@ let make_autogoal_hints =
fun only_classes ?(st=full_transparent_state) g ->
let sign = pf_filtered_hyps g in
match freeze () with
- | Some (sign', hints) when Environ.eq_named_context_val sign sign' -> hints
+ | Some (onlyc, sign', hints)
+ when onlyc = only_classes &&
+ Environ.eq_named_context_val sign sign' -> hints
| _ -> let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in
- unfreeze (Some (sign, hints)); hints
+ unfreeze (Some (only_classes, sign, hints)); hints
let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac =
{ skft = fun sk fk {it = gl,hints; sigma=s} ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 1c5e4b2f..0385063f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -236,15 +236,27 @@ let register_general_rewrite_clause = (:=) general_rewrite_clause
let is_applied_rewrite_relation = ref (fun _ _ _ _ -> None)
let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation
+(* Do we have a JMeq instance on twice the same domains ? *)
+
+let jmeq_same_dom gl = function
+ | None -> true (* already checked in Hipattern.find_eq_data_decompose *)
+ | Some t ->
+ let rels, t = decompose_prod_assum t in
+ let env = Environ.push_rel_context rels (pf_env gl) in
+ match decompose_app t with
+ | _, [dom1; _; dom2;_] -> is_conv env (project gl) dom1 dom2
+ | _ -> false
+
(* find_elim determines which elimination principle is necessary to
eliminate lbeq on sort_of_gl. *)
-let find_elim hdcncl lft2rgt dep cls args gl =
- let inccl = (cls = None) in
- if (eq_constr hdcncl (constr_of_reference (Coqlib.glob_eq)) ||
- eq_constr hdcncl (constr_of_reference (Coqlib.glob_jmeq)) &&
- pf_conv_x gl (List.nth args 0) (List.nth args 2)) && not dep
- || Flags.version_less_or_equal Flags.V8_2
+let find_elim hdcncl lft2rgt dep cls ot gl =
+ let inccl = not (Option.has_some cls) in
+ let hdcncl_is u = eq_constr hdcncl (constr_of_reference u) in
+ if (hdcncl_is (Coqlib.glob_eq) ||
+ hdcncl_is (Coqlib.glob_jmeq) && jmeq_same_dom gl ot)
+ && not dep
+ || Flags.version_less_or_equal Flags.V8_2
then
match kind_of_term hdcncl with
| Ind ind_sp ->
@@ -295,7 +307,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars frze
let isatomic = isProd (whd_zeta hdcncl) in
let dep_fun = if isatomic then dependent else dependent_no_evar in
let dep = dep_proof_ok && dep_fun c (type_of_clause gl cls) in
- let elim = find_elim hdcncl lft2rgt dep cls (snd (decompose_app t)) gl in
+ let elim = find_elim hdcncl lft2rgt dep cls (Some t) gl in
general_elim_clause with_evars frzevars tac cls sigma c t l
(match lft2rgt with None -> false | Some b -> b)
{elimindex = None; elimbody = (elim,NoBindings)} gl
@@ -1208,7 +1220,7 @@ let swapEquandsInConcl gls =
let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
(* find substitution scheme *)
- let eq_elim = find_elim lbeq.eq (Some false) false None [e1;e2] gls in
+ let eq_elim = find_elim lbeq.eq (Some false) false None None gls in
(* build substitution predicate *)
let p = lambda_create (pf_env gls) (t,body) in
(* apply substitution scheme *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7479ee9a..c2eaa327 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -227,7 +227,7 @@ let add_tactic s t =
let overwriting_add_tactic s t =
if Hashtbl.mem tac_tab s then begin
Hashtbl.remove tac_tab s;
- warning ("Overwriting definition of tactic "^s)
+ msg_warn ("Overwriting definition of tactic "^s)
end;
Hashtbl.add tac_tab s t
@@ -265,7 +265,7 @@ let lookup_genarg id =
try Gmap.find id !extragenargtab
with Not_found ->
let msg = "No interpretation function found for entry " ^ id in
- warning msg;
+ msg_warn msg;
let f = (fun _ _ -> failwith msg), (fun _ _ _ -> failwith msg), (fun _ a -> a) in
add_interp_genarg id f;
f