aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/term_dnet.mli
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | We do up to `Term` which is the main bulk of the changes.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* refresh metas in rewrite hints loaded from .vo files (fix bug #3815)Gravatar Nickolai Zeldovich2015-04-06
| | | | | | | | | | | | | | | | | | 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).
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Moving Dnet-related code to tactics/.Gravatar Pierre-Marie Pédrot2014-05-08