| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-03-18 | Update headers in the whole code base. | Théo Zimmermann | |
| Add headers to a few files which were missing them. | |||
| 2019-11-21 | [coq] Untabify the whole ML codebase. | Emilio Jesus Gallego Arias | |
| We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ``` | |||
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann | |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2016-01-20 | Update copyright headers. | Maxime Dénès | |
| 2015-04-06 | refresh metas in rewrite hints loaded from .vo files (fix bug #3815) | Nickolai Zeldovich | |
| 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). | |||
| 2015-02-23 | Fix some typos in comments. | Guillaume Melquiond | |
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2014-05-08 | Moving Dnet-related code to tactics/. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |