From d2c5c5e616a6e118291fe1ce9965c731adac03a8 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 19 Jan 2014 15:09:23 +0100
Subject: Imported Upstream version 8.4pl3dfsg

---
 tactics/class_tactics.ml4 |  8 +++++---
 tactics/equality.ml       | 28 ++++++++++++++++++++--------
 tactics/tacinterp.ml      |  4 ++--
 3 files changed, 27 insertions(+), 13 deletions(-)

(limited to 'tactics')

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
-- 
cgit v1.2.3