Merge branch 'v8.5' into trunk

7 files changed, 31 insertions, 4 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index ee8e1855d5..4eb8a79256 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -211,6 +211,7 @@ let cache_hintrewrite (_,(rbase,lrl)) =
   let base = try raw_find_base rbase with Not_found -> HintDN.empty in
   let max = try fst (Util.List.last (HintDN.find_all base)) with Failure _ -> 0
   in
+  let lrl = HintDN.refresh_metas lrl in
   let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in
     rewtab:=String.Map.add rbase (HintDN.union lrl base) !rewtab
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c0fe514f08..244f9a727d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -350,7 +350,9 @@ let make_autogoal_hints =
       let sign = pf_filtered_hyps g in
       let (onlyc, sign', cached_hints) = !cache in
 	if onlyc == only_classes && 
-	  (sign == sign' || Environ.eq_named_context_val sign sign') then
+	  (sign == sign' || Environ.eq_named_context_val sign sign') 
+	  && Hint_db.transparent_state cached_hints == st
+	then
 	  cached_hints
 	else
 	  let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in
diff --git a/tactics/dnet.ml b/tactics/dnet.ml
index bb71620c09..93334db73c 100644
--- a/tactics/dnet.ml
+++ b/tactics/dnet.ml
@@ -39,6 +39,7 @@ sig
   val inter : t -> t -> t
   val union : t -> t -> t
   val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t
+  val map_metas : (meta -> meta) -> t -> t
 end
 
 module Make =
@@ -288,4 +289,13 @@ struct
       | Node e -> Node (T.map (map sidset sterm) e) in
     Nodes (tmap_map sterm snode t, Mmap.map (idset_map sidset) m)
 
+  let rec map_metas f (Nodes (t, m)) : t =
+    let f_node = function
+      | Terminal (e, is) -> Terminal (T.map (map_metas f) e, is)
+      | Node e -> Node (T.map (map_metas f) e)
+    in
+    let m' = Mmap.fold (fun m s acc -> Mmap.add (f m) s acc) m Mmap.empty in
+    let t' = Tmap.fold (fun k n acc -> Tmap.add k (f_node n) acc) t Tmap.empty in
+    Nodes (t', m')
+
 end
diff --git a/tactics/dnet.mli b/tactics/dnet.mli
index 4bfa7263e9..52853d7021 100644
--- a/tactics/dnet.mli
+++ b/tactics/dnet.mli
@@ -113,6 +113,8 @@ sig
 
   (** apply a function on each identifier and node of terms in a dnet *)
   val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t
+
+  val map_metas : (meta -> meta) -> t -> t
 end
 
 module Make :
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 838f8865d0..bcfd6657e0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1230,8 +1230,6 @@ let try_delta_expand env sigma t =
 let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
 let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 
-let eqdep_dec = qualid_of_string "Coq.Logic.Eqdep_dec"
-
 let inject_if_homogenous_dependent_pair ty =
   Proofview.Goal.nf_enter begin fun gl ->
   try
@@ -1254,7 +1252,7 @@ let inject_if_homogenous_dependent_pair ty =
     (* knows inductive types *)
     if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
       pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
-    Library.require_library [Loc.ghost,eqdep_dec] (Some false);
+    Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
     let new_eq_args = [|pf_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e637b2e36d..e79fc6dc9a 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -371,6 +371,17 @@ struct
   let find_all dn = Idset.elements (TDnet.find_all dn)
 
   let map f dn = TDnet.map f (fun x -> x) dn
+
+  let refresh_metas dn =
+    let new_metas = ref Int.Map.empty in
+    let refresh_one_meta i =
+      try Int.Map.find i !new_metas
+      with Not_found ->
+        let new_meta = fresh_meta () in
+        let () = new_metas := Int.Map.add i new_meta !new_metas in
+        new_meta
+    in
+    TDnet.map_metas refresh_one_meta dn
 end
 
 module type S =
@@ -385,4 +396,5 @@ sig
   val search_pattern : t -> constr -> ident list
   val find_all : t -> ident list
   val map : (ident -> ident) -> t -> t
+  val refresh_metas : t -> t
 end
diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli
index a5c80cc00e..58f95ac6c9 100644
--- a/tactics/term_dnet.mli
+++ b/tactics/term_dnet.mli
@@ -80,6 +80,8 @@ sig
   val find_all : t -> ident list
 
   val map : (ident -> ident) -> t -> t
+
+  val refresh_metas : t -> t
 end
 
 module Make :