aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Compat
Commit message (Expand)AuthorAge
* Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gravatar Gaëtan Gilbert2017-11-28
* Compat/Coq87.v : Unset Omega UseLocalDefs (see PR #768)Gravatar Pierre Letouzey2017-10-07
* Adding a V8.7 compatibility version number.Gravatar Hugo Herbelin2017-07-21
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Put plugin exports in the right compatibility fileGravatar Jason Gross2017-06-22
* Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\
* | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| * Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
|/
* drop vo.itarget files and compute the corresponding the corresponding values ...Gravatar Matej Kosik2017-06-01
* Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
|\
| * More explicit name for status of unification constraints.Gravatar Maxime Dénès2016-11-07
* | Silence option deprecation warnings in the compat fileGravatar Jason Gross2016-11-04
| * Add Unset Use Unif Heuristics in Compat/Coq85Gravatar Matthieu Sozeau2016-10-22
|/
* Fix previous commit.Gravatar Pierre-Marie Pédrot2016-10-17
* Merge PR #300 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
|\
* | Clean up type classes flags and update compat file.Gravatar Maxime Dénès2016-10-05
| * Move vector/list compat notations to their relevant filesGravatar Jason Gross2016-09-29
|/
* Remove spaces from around list notationsGravatar Jason Gross2016-09-26
* Unbreak Ltac [ | .. | ] notation in -compat 8.5Gravatar Jason Gross2016-09-26
* Fix bug #4785 (use [ ] for vector nil)Gravatar Jason Gross2016-09-26
* Refolding: disable in 8.4 compat file, documentGravatar Matthieu Sozeau2016-09-12
* no-refold patchGravatar Paul Steckler2016-09-09
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-02
|\
| * Fix bug #5043: [Admitted] lemmas pick up section variables.Gravatar Pierre-Marie Pédrot2016-08-31
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\|
* | Fix #4793: Coq 8.6 should accept -compat 8.6Gravatar Maxime Dénès2016-07-06
| * Compat84: Don't mess with stdlib modulesGravatar Jason Gross2016-07-05
* | Add Unset Shrink Abstract/Obligations in Coq85Gravatar Matthieu Sozeau2016-06-27
* | Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
| * Unbreak singleton list-like notation (-compat 8.4)Gravatar Jason Gross2016-06-09
* | Relying instead on the Coq85 inclusion!Gravatar Hugo Herbelin2016-06-06
* | Mode "Bracketing Last Introduction Pattern" is on for 8.4Gravatar Hugo Herbelin2016-06-06
* | Mode "Regular Subst Tactic" is on in 8.6.Gravatar Hugo Herbelin2016-06-06
* | Merge remote-tracking branch 'github/pr/118' into trunkGravatar Maxime Dénès2016-06-06
|\ \
* \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-20
|\ \ \ | | |/ | |/|
| * | Removing unexcepted activation of option "Regular Subst Tactic", sinceGravatar Hugo Herbelin2016-05-14
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\| |
| * | Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...Gravatar Pierre Letouzey2016-05-04
| |\ \
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-09
|\| | |
| * | | 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
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| | |
| * | | Update copyright headers.Gravatar Maxime Dénès2016-01-20
| | | * Update Coq84.vGravatar Jason Gross2016-01-12
| |_|/ |/| |
| | * Move compatibility notations to their proper filesGravatar Jason Gross2015-12-29
| |/
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-15
|\|
| * Moved proof_admitted to its own file, named "AdmitAxiom.v".Gravatar Maxime Dénès2015-12-14