aboutsummaryrefslogtreecommitdiff
path: root/theories/Compat/Coq85.v
AgeCommit message (Expand)Author
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-22Put plugin exports in the right compatibility fileJason Gross
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2016-11-07Merge commit 'e6edb33' into v8.6Maxime Dénès
2016-11-07More explicit name for status of unification constraints.Maxime Dénès
2016-11-04Silence option deprecation warnings in the compat fileJason Gross
2016-10-22Add Unset Use Unif Heuristics in Compat/Coq85Matthieu Sozeau
2016-10-17Fix previous commit.Pierre-Marie Pédrot
2016-10-05Clean up type classes flags and update compat file.Maxime Dénès
2016-09-26Unbreak Ltac [ | .. | ] notation in -compat 8.5Jason Gross
2016-09-26Fix bug #4785 (use [ ] for vector nil)Jason Gross
2016-09-09no-refold patchPaul Steckler
2016-07-06Fix #4793: Coq 8.6 should accept -compat 8.6Maxime Dénès
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-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-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-11-10Updating Compat85.v after bd1c97653 on bracketing last or-andHugo Herbelin
2015-09-30Add compatibility files (feature 4319)Jason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 20:26:24 +0000