diff options
| author |  Nickolai Zeldovich <nickolai@csail.mit.edu> | 2015-04-03 07:24:42 -0400 |
|---|---|---|
| committer |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-04-06 08:52:16 +0200 |
| commit | 5d03ea0729ff1ed01bf64e9c98355149bb4c04e9 (patch) | |
| tree | e02886fa349d6c6805a603b8656a0f15079a6edd /tactics/dnet.mli | |
| parent | b667f6fec675d3a05ba0475bdb84beaeed7622ac (diff) | |
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).
Diffstat (limited to 'tactics/dnet.mli')
| -rw-r--r-- | tactics/dnet.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/dnet.mli b/tactics/dnet.mli index 4bfa7263e..52853d702 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 : |