aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Compat
Commit message (Expand)AuthorAge
* Fix bug #5043: [Admitted] lemmas pick up section variables.Gravatar Pierre-Marie Pédrot2016-08-31
* Compat84: Don't mess with stdlib modulesGravatar Jason Gross2016-07-05
* Unbreak singleton list-like notation (-compat 8.4)Gravatar Jason Gross2016-06-09
* Removing unexcepted activation of option "Regular Subst Tactic", sinceGravatar Hugo Herbelin2016-05-14
* Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...Gravatar Pierre Letouzey2016-05-04
|\
* | Added compatibility coercions from Specif.v which were present in Coq 8.4.Gravatar Hugo Herbelin2016-04-08
* | Add -compat 8.4 econstructor tactics, and testsGravatar Jason Gross2016-04-05
* | Fix bug #4656Gravatar Jason Gross2016-04-05
* | Update Coq84.vGravatar Jason Gross2016-04-04
* | Add compatibility Nonrecursive Elimination SchemesGravatar Jason Gross2016-04-04
* | Update copyright headers.Gravatar Maxime Dénès2016-01-20
| * Move compatibility notations to their proper filesGravatar Jason Gross2015-12-29
|/
* Moved proof_admitted to its own file, named "AdmitAxiom.v".Gravatar Maxime Dénès2015-12-14
* Update compatibility file for some of bug #4392Gravatar Jason Gross2015-11-03
* Add compatibility files (feature 4319)Gravatar Jason Gross2015-09-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 17:29:32 +0000