From f15506263b0f85039b0b3c25c93406b9f9a5f241 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 1 Apr 2015 11:14:21 +0200 Subject: Removing a probably incorrect on-the-fly require in a tactic. Also removed the require function it was using, as it is absent from the remaining of the code. --- tactics/equality.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'tactics') 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 -- cgit v1.2.3 From 5d03ea0729ff1ed01bf64e9c98355149bb4c04e9 Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Fri, 3 Apr 2015 07:24:42 -0400 Subject: refresh metas in rewrite hints loaded from .vo files (fix bug #3815) Meta variables in rewrite rules are named by integers that are allocated sequentially at runtime (fresh_meta in tactics/term_dnet.ml). This causes a problem when some rewrite rules (with meta variables) are generated by coqc, saved in a .vo file, and then imported into another coqc/coqtop process. The new process will allocate its own meta variable numbers starting from 0, colliding with existing imported meta variable numbers. One manifestation of this issue was various failures of [rewrite_strat]; see bug #3815 for examples. This change fixes the problem, by replacing all meta variable numbers in imported rewrite rules at import time. This seems to fix the various failures reported in bug #3815. Thanks to Jason Gross for tracking down the commit that introduced this bug in the first place (71a9b7f2). --- tactics/autorewrite.ml | 1 + tactics/dnet.ml | 10 ++++++++++ tactics/dnet.mli | 2 ++ tactics/term_dnet.ml | 12 ++++++++++++ tactics/term_dnet.mli | 2 ++ 5 files changed, 27 insertions(+) (limited to 'tactics') 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/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/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 : -- cgit v1.2.3 From 400d3dcca26bba32d6e170ef36468e6c5425a2ed Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 9 Apr 2015 07:36:02 +0200 Subject: Fix caching of local hintdb in typeclasses eauto. --- tactics/class_tactics.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index e97a42e6e4..98266a4b6c 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 -- cgit v1.2.3