aboutsummaryrefslogtreecommitdiff
path: root/theories/Compat
AgeCommit message (Expand)Author
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-20Update copyright headers.Maxime Dénès
2015-12-14Moved proof_admitted to its own file, named "AdmitAxiom.v".Maxime Dénès
2015-11-03Update compatibility file for some of bug #4392Jason Gross
2015-09-30Add compatibility files (feature 4319)Jason Gross