Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | * | | | | | | | | | | | | | | | | Fix the introduction of SSR refman chapter. | Théo Zimmermann | 2017-09-08 | |
| |_|_|_|/ / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | * | | | | | Parse directly to Sorts.family when appropriate. | Gaëtan Gilbert | 2017-09-08 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | * | | | | | | | | | | | | | | Move README.ci and link to it from CONTRIBUTING. | Théo Zimmermann | 2017-09-08 | |
| | | | | * | | | | | | | | | | | | | | Update CI policy. | Théo Zimmermann | 2017-09-08 | |
* | | | | | | | | | | | | | | | | | | | Merge PR #997: coqdoc: Support comments in verbatim output | Maxime Dénès | 2017-09-07 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | Merge PR #1016: 2 Typos in 'Add Parametric Morphism' Documentation | Maxime Dénès | 2017-09-07 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #968: Better error messages on the CI | Maxime Dénès | 2017-09-07 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #931: Parametrize module body | Maxime Dénès | 2017-09-07 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #914: Making the detyper lazy | Maxime Dénès | 2017-09-07 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #904: Add build_coq_or to API.Coqlib | Maxime Dénès | 2017-09-07 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | | | * | | | | | use get_arguments, String.concat, remove -I | Paul Steckler | 2017-09-06 | |
| | | | | | | | | | * | | | | | | | | | | | | | | Fix a refine anomaly "Evar defined twice". | Pierre-Marie Pédrot | 2017-09-06 | |
* | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #1022: Appveyor package | Maxime Dénès | 2017-09-06 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | | | | * | | | | | read flags from project file for Compile Buffer | Paul Steckler | 2017-09-05 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | | | Make AppVeyor generate Windows package. | Maxime Dénès | 2017-09-05 | |
| * | | | | | | | | | | | | | | | | | | | | | | | Remove -debug option from Windows build script. | Maxime Dénès | 2017-09-05 | |
| * | | | | | | | | | | | | | | | | | | | | | | | Get sources of cygwin packages after building the installer. | Maxime Dénès | 2017-09-05 | |
| * | | | | | | | | | | | | | | | | | | | | | | | Adapt Windows build script to new CoqIDE data installation directory. | Maxime Dénès | 2017-09-05 | |
| * | | | | | | | | | | | | | | | | | | | | | | | Print more of the Coq build output. | Maxime Dénès | 2017-09-05 | |
| * | | | | | | | | | | | | | | | | | | | | | | | Print Coq build output. | Maxime Dénès | 2017-09-05 | |
| * | | | | | | | | | | | | | | | | | | | | | | | In regression test mode, run cygwin setup to install dependencies. | Maxime Dénès | 2017-09-05 | |
|/ / / / / / / / / / / / / / / / / / / / / / / | ||||
* | | | | | | | | | | | | | | | | | | | | | | | Merge PR #1011: fix test-suite/coq-makefile/findlib-package on windows after ... | Maxime Dénès | 2017-09-05 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | Merge PR #1020: .mailmap update | Guillaume Melquiond | 2017-09-05 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1010: Move mention of native_compute profiling in CHANGES | Maxime Dénès | 2017-09-05 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1021: Fix Software Foundations build. | Maxime Dénès | 2017-09-05 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | * | | | | | | | | | | | | | | | | | | | | | | | .mailmap update | Gaëtan Gilbert | 2017-09-05 | |
| |_|/ / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | | | | Fix Software Foundations build. | Maxime Dénès | 2017-09-05 | |
|/ / / / / / / / / / / / / / / / / / / / / / / / | ||||
| | | | | | | | | | | | | | | | | | | | * | | | | Update CREDITS on a best-effort basis. | Théo Zimmermann | 2017-09-05 | |
| | * | | | | | | | | | | | | | | | | | | | | | | fix test-suite/coq-makefile/findlib-package on windows | Enrico Tassi | 2017-09-04 | |
| |/ / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | Merge PR #1018: Avoid reinstalling some Cygwin dependencies on AppVeyor. | Maxime Dénès | 2017-09-04 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | | | | | | | | | | | | | | Avoid reinstalling some Cygwin dependencies on AppVeyor. | Maxime Dénès | 2017-09-04 | |
|/ / / / / / / / / / / / / / / / / / / / / / / | ||||
| | | * / / / / / / / / / / / / / / / / / / / | Making detyping potentially lazy. | Pierre-Marie Pédrot | 2017-09-04 | |
| |_|/ / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | | | | | | | | Addressing BZ#5713 (classical_left/classical_right artificially restricted). | Hugo Herbelin | 2017-09-03 | |
| |_|_|_|_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | ||||
| | | | | * | | | | | | | | | | | | | | | | 2 Typos in 'Add Parametric Morphism' Documentation | staffehn | 2017-09-03 | |
| |_|_|_|/ / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | * | | | | | | | | | | | | add option index entry for NativeCompute Profiling | Paul Steckler | 2017-09-01 | |
| |_|_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | move mention of native_compute profiling in CHANGES | Paul Steckler | 2017-09-01 | |
|/ / / / / / / / / / / / / / / / / / | ||||
| | | | | | | | | * / / / / / / / / | Do not hashcons universes beforehand. | Pierre-Marie Pédrot | 2017-09-01 | |
| |_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | Bump MacOS version number and magic numbers. | Maxime Dénès | 2017-09-01 | |
* | | | | | | | | | | | | | | | | | Change version string to 8.8+alpha. | Maxime Dénès | 2017-09-01 | |
| | | | | | * | | | | | | | | | | | Document primitive projections in more detail | Matthieu Sozeau | 2017-08-31 | |
| | | | | | * | | | | | | | | | | | RefMan-ssr: fix warning | Matthieu Sozeau | 2017-08-31 | |
| | | | | | | | | | | | | | | * | | Fix install-doc target | Gaëtan Gilbert | 2017-08-31 | |
* | | | | | | | | | | | | | | | | | Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name | Maxime Dénès | 2017-08-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | Merge PR #992: Fix BZ#5687: Coqtop died badly modal message box from CoqIDE. | Maxime Dénès | 2017-08-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #993: Credits for version 8.7 | Maxime Dénès | 2017-08-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | | | | | | | | | Credits for version 8.7 | Matthieu Sozeau | 2017-08-31 | |
* | | | | | | | | | | | | | | | | | | | Merge PR #999: For BZ#5688, mention hanging issue in ocamldebug and workaround | Maxime Dénès | 2017-08-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #996: Fix BZ#5697: Congruence does not work with primitive projections | Maxime Dénès | 2017-08-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #995: Program: fix BZ#5683, missing lift when building case predicate | Maxime Dénès | 2017-08-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flag | Maxime Dénès | 2017-08-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |