| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-01-18 | Support locality attributes for Hint Rewrite (including export) | Gaëtan Gilbert | |
| We deprecate unspecified locality as was done for Hint. Close #13724 | |||
| 2018-10-04 | test-suite: cleaning | Vincent Laporte | |
| 2011-06-18 | Relaxed the constraint introduced in r14190 that froze the existing | herbelin | |
| evars when rewriting. Use it for autorewrite and subst. Accept evars instantiation in multi_rewrite so that rewrite alone remains compatible (it is used in contribs, e.g. Godel, in places where it does not seem absurd to allow it), but there are no good reason for it. Comments welcome. + addition of some tests for rewriting (one being related to commit 14217) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14222 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |