Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey | 2017-06-14 |
* | Merge PR#498: Bignums as a separate opam package | Maxime Dénès | 2017-06-14 |
|\ | |||
* \ | Merge PR#385: Equality of sigma types | Maxime Dénès | 2017-06-13 |
|\ \ | |||
* \ \ | Merge PR#757: Better sectioning on travis log printing in test-suite | Maxime Dénès | 2017-06-13 |
|\ \ \ | |||
| | | * | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey | 2017-06-13 |
| |_|/ |/| | | |||
* | | | Merge PR#709: Bytecode compilation apart from 'make world', again | Maxime Dénès | 2017-06-12 |
|\ \ \ | |||
* | | | | Add support for "-bypass-API" argument of "coq_makefile" | Matej Košík | 2017-06-12 |
* | | | | make test-suite/save-logs.sh usable also on old MacOS X | Maxime Denes | 2017-06-12 |
| | * | | Fix Travis sectioning | Jason Gross | 2017-06-10 |
| | * | | Better sectioning on travis log printing in test-suite | Jason Gross | 2017-06-09 |
| |/ / |/| | | |||
* | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-06-08 |
|\ \ \ | |||
* \ \ \ | Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh... | Maxime Dénès | 2017-06-06 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR#600: Some factorizations of ltac interpretation functions between ss... | Maxime Dénès | 2017-06-06 |
|\ \ \ \ \ | |||
* | | | | | | Drop '.' from CErrors.anomaly, insert it in args | Jason Gross | 2017-06-02 |
* | | | | | | Merge PR#691: [travis] Add OSX test-suite checking. | Maxime Dénès | 2017-06-02 |
|\ \ \ \ \ \ | |||
| | | | * \ \ | Merge PR#705: Fix bug #5019 (looping zify on dependent types) | Maxime Dénès | 2017-06-02 |
| | | | |\ \ \ | |||
* | | | | \ \ \ | Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel. | Maxime Dénès | 2017-06-02 |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR#711: [gitlab] Artifact test suite logs on failure. | Maxime Dénès | 2017-06-02 |
|\ \ \ \ \ \ \ \ \ | |||
| | | * | | | | | | | Test-suite: do not test native compiler if disabled by configure. | Maxime Dénès | 2017-06-01 |
| | | | | | | | * | | test-suite/coq-makefile: we do not build byte file by default anymore | Pierre Letouzey | 2017-06-01 |
* | | | | | | | | | | Merge PR#449: make specialize smarter (bug 5370). | Maxime Dénès | 2017-06-01 |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | * | | | | | | | | [emacs] [toplevel] Make emacs flag local to the toplevel. | Emilio Jesus Gallego Arias | 2017-06-01 |
| | | | | | | * | | | | Merge PR#631: Fix bug #5255 | Maxime Dénès | 2017-06-01 |
| | | | | | | |\ \ \ \ | |||
| | | | * | | | | | | | | Fix coq_makefile uninstall target under OSX. | Maxime Dénès | 2017-06-01 |
| | | |/ / / / / / / / | |||
* | | | | | | | | | | | Merge PR#694: Fixing #5523 (missing support for complex constructions in recu... | Maxime Dénès | 2017-06-01 |
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / |/| | | | | | | | | | | |||
| | | | | | | | * | | | Fix bug #5019 (looping zify on dependent types) | Jason Gross | 2017-06-01 |
| | | | | | | | * | | | Add opened bug 5019 | Jason Gross | 2017-06-01 |
| | | | | | * | | | | | Merge PR#710: Add test-suite checks for coqchk with constraints | Maxime Dénès | 2017-06-01 |
| | | | | | |\ \ \ \ \ | | | | | | | |_|/ / / | | | | | | |/| | | | | |||
* | | | | | | | | | | | Merge PR#704: Fix empty parentheses display in test-suite | Maxime Dénès | 2017-06-01 |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR#701: [readlink -f] doesn't work on OSX | Maxime Dénès | 2017-05-31 |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | * | | | | | | | | [travis] print failing test suite logs on failure | Gaëtan Gilbert | 2017-05-31 |
| | | | | | | | * | | | | | Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake (... | Maxime Dénès | 2017-05-31 |
| | | | | | | | |\ \ \ \ \ | |||
| | | | * | | | | | | | | | | Tests for new specialize feature + CHANGES. | Pierre Courtieu | 2017-05-31 |
| | | | | |_|_|_|_|_|_|/ / | | | | |/| | | | | | | | | |||
| | | | | | | | * | | | | | Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with secti... | Maxime Dénès | 2017-05-31 |
| | | | | | | | |\ \ \ \ \ | |||
| | | | | | * | | | | | | | | Factorizing interp_gen through a function interpreting glob_constr. | Hugo Herbelin | 2017-05-31 |
| | | | | |/ / / / / / / / | | | | |/| | | | | | | | | |||
| | | | | | * | | | | | | | More precise on preventing clash between bound vars name and hidden impargs. | Hugo Herbelin | 2017-05-31 |
| | | | | | * | | | | | | | Fixing #5233 (missing implicit arguments for recursive records). | Hugo Herbelin | 2017-05-31 |
| | | | | | * | | | | | | | Fixing a failure to interpret some local implicit arguments in Inductive. | Hugo Herbelin | 2017-05-31 |
| | | | | |/ / / / / / / | | | | |/| | | | | | | | |||
| | | * | | | | | | | | | Fixing #5523 (missing support for complex constructions in recursive notations). | Hugo Herbelin | 2017-05-31 |
| | | * | | | | | | | | | Fixing a too lax constraint for finding recursive binder part of a notation. | Hugo Herbelin | 2017-05-31 |
| | | |/ / / / / / / / | |||
| | | | * / / / / / / | [gitlab] Artifact test suite logs on failure. | Gaëtan Gilbert | 2017-05-30 |
| | | |/ / / / / / / | |||
| | | | | | | * / / | Add test-suite checks for coqchk with constraints | Jason Gross | 2017-05-30 |
| | | | | |_|/ / / | | | | |/| | | | | |||
| | * | / | | | | | Fix empty parentheses display in test-suite | Jason Gross | 2017-05-30 |
| | |/ / / / / / | |||
| | | * | | | | | Merge PR#693: A subtle bug in tclWITHHOLES. | Maxime Dénès | 2017-05-30 |
| | | |\ \ \ \ \ | |||
| * | | | | | | | | [readlink -f] doesn't work on OSX | Gaëtan Gilbert | 2017-05-30 |
| |/ / / / / / / | |||
* | | | | | | | | Support for using type information to infer more precise evar sources. | Hugo Herbelin | 2017-05-30 |
* | | | | | | | | Few tests for e-variants of assert, set, remember. | Hugo Herbelin | 2017-05-30 |
|/ / / / / / / | |||
| | | * | | | | Fix bug 5550: "typeclasses eauto with" does not work with section variables. | Théo Zimmermann | 2017-05-30 |
* | | | | | | | Merge PR#687: Gitlab CI | Maxime Dénès | 2017-05-29 |
|\ \ \ \ \ \ \ | |||
| | * | | | | | | Omega: use "simpl" only on coefficents, not on atoms (fix #4132) | Pierre Letouzey | 2017-05-29 |
| | | |/ / / / | | |/| | | | |