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/term_dnet.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'tactics/term_dnet.ml') diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index e637b2e36..e79fc6dc9 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 -- cgit v1.2.3