aboutsummaryrefslogtreecommitdiff
path: root/theories/Compat
AgeCommit message (Expand)Author
2016-08-31Fix bug #5043: [Admitted] lemmas pick up section variables.Pierre-Marie Pédrot
2016-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-06Fix #4793: Coq 8.6 should accept -compat 8.6Maxime Dénès
2016-07-05Compat84: Don't mess with stdlib modulesJason Gross
2016-06-27Add Unset Shrink Abstract/Obligations in Coq85Matthieu Sozeau
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-09Unbreak singleton list-like notation (-compat 8.4)Jason Gross
2016-06-06Relying instead on the Coq85 inclusion!Hugo Herbelin
2016-06-06Mode "Bracketing Last Introduction Pattern" is on for 8.4Hugo Herbelin
2016-06-06Mode "Regular Subst Tactic" is on in 8.6.Hugo Herbelin
2016-06-06Merge remote-tracking branch 'github/pr/118' into trunkMaxime Dénès
2016-05-20Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-14Removing unexcepted activation of option "Regular Subst Tactic", sinceHugo Herbelin
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-04Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...Pierre Letouzey
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-08Added compatibility coercions from Specif.v which were present in Coq 8.4.Hugo Herbelin
2016-04-05Add -compat 8.4 econstructor tactics, and testsJason Gross
2016-04-05Fix bug #4656Jason Gross
2016-04-04Update Coq84.vJason Gross
2016-04-04Add compatibility Nonrecursive Elimination SchemesJason Gross
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-12Update Coq84.vJason Gross
2015-12-29Move compatibility notations to their proper filesJason Gross
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-14Moved proof_admitted to its own file, named "AdmitAxiom.v".Maxime Dénès
2015-11-10Updating Compat85.v after bd1c97653 on bracketing last or-andHugo Herbelin
2015-11-03Update compatibility file for some of bug #4392Jason Gross
2015-09-30Add compatibility files (feature 4319)Jason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:04:22 +0000