aboutsummaryrefslogtreecommitdiff
path: root/theories/Compat
AgeCommit message (Expand)Author
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2020-11-23Update compat infrastructure for 8.14Enrico Tassi
2020-11-15Update compate Coq812.vGaëtan Gilbert
2020-11-09[compat] remove 8.10Enrico Tassi
2020-05-18Update to 8.13.Théo Zimmermann
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-08Remove -compat 8.9.Théo Zimmermann
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-11Run update-compat script with --release option.Théo Zimmermann
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-04-02Remove -compat 8.7Jason Gross
2019-02-04Primitive integersMaxime Dénès
2019-01-24Update -compat to support -compat 8.10Jason Gross
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-22Disable deprecation warnings in compat files.Gaëtan Gilbert
2018-10-23Compat 8.8: For String/Ascii, hides "Declare ML Module" behind an "Export".Hugo Herbelin
2018-10-02Update the -compat flagsJason Gross
2018-08-31Make Numeral Notation follow Import, not RequireJason Gross
2018-03-07Add empty compat file for Coq 8.8Jason Gross
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-28Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gaëtan Gilbert
2017-10-07Compat/Coq87.v : Unset Omega UseLocalDefs (see PR #768)Pierre Letouzey
2017-07-21Adding a V8.7 compatibility version number.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-22Put plugin exports in the right compatibility fileJason Gross
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2017-06-14Remove support for Coq 8.4.Guillaume Melquiond
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
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-17Merge PR #300 into v8.6Pierre-Marie Pédrot
2016-10-05Clean up type classes flags and update compat file.Maxime Dénès
2016-09-29Move vector/list compat notations to their relevant filesJason Gross
2016-09-26Remove spaces from around list notationsJason Gross
2016-09-26Unbreak Ltac [ | .. | ] notation in -compat 8.5Jason Gross
2016-09-26Fix bug #4785 (use [ ] for vector nil)Jason Gross
2016-09-12Refolding: disable in 8.4 compat file, documentMatthieu Sozeau
2016-09-09no-refold patchPaul Steckler
2016-09-02Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:36:51 +0000