Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | | | | | | | | | | | | | | | | | | | | Fixing bug #5693 (treating empty notation format as any format). | Hugo Herbelin | 2017-09-12 | |
| * | | | | | | | | | | | | | | | | | | | | Adding a missing period in a notation warning. | Hugo Herbelin | 2017-09-12 | |
| * | | | | | | | | | | | | | | | | | | | | Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding. | Hugo Herbelin | 2017-09-12 | |
| * | | | | | | | | | | | | | | | | | | | | Don't exclude a priori CLocalDef to be treated by ppconstr.ml. | Hugo Herbelin | 2017-09-12 | |
| * | | | | | | | | | | | | | | | | | | | | Fixing a typo in printing notations with recursive binders. | Hugo Herbelin | 2017-09-12 | |
| * | | | | | | | | | | | | | | | | | | | | Fixing a bug of recursive notations introduced in dfdaf4de. | Hugo Herbelin | 2017-09-12 | |
| * | | | | | | | | | | | | | | | | | | | | Fixing little inaccuracy in coercions to ident or name. | Hugo Herbelin | 2017-09-12 | |
|/ / / / / / / / / / / / / / / / / / / / | ||||
| | | | | | | | | | | | | | * / / / / / | Port is_Set and is_Type to EConstr, as was is_Prop already. | Guillaume Melquiond | 2017-09-12 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | * | | | | | | Better error messages, fix for BZ#5723 | Paul Steckler | 2017-09-11 | |
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | Merge PR #1017: Addressing BZ#5713 (classical_left/classical_right artificial... | Maxime Dénès | 2017-09-11 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | * | | | | | | Remove unneeded fix for BZ#1715 | Gaëtan Gilbert | 2017-09-11 | |
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | Merge PR #1032: Make our CI policy clearer and more explicit | Maxime Dénès | 2017-09-11 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | * | | Disable OSX signing for temporary artifacts. | Maxime Dénès | 2017-09-11 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit` | Maxime Dénès | 2017-09-11 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1035: Fix the introduction of SSR refman chapter. | Maxime Dénès | 2017-09-11 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1029: Fix a refine anomaly "Evar defined twice". | Maxime Dénès | 2017-09-11 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1014: Add option index entry for NativeCompute Profiling | Maxime Dénès | 2017-09-11 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1004: Document primitive projections in more detail | Maxime Dénès | 2017-09-11 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #987: In Array.smartmap, read and write from same array | Maxime Dénès | 2017-09-11 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | | | * | | | | | In stm, fixing a typo about flushing debugging messages. | Hugo Herbelin | 2017-09-11 | |
| | | | | | | | | | | | | | | | | | | * | | | | | Typo in the header of ide_slave.ml. | Hugo Herbelin | 2017-09-11 | |
| | | | | | | | | | | | | | | | | | | * | | | | | Coqide: adding a separating space in some debugging messages. | Hugo Herbelin | 2017-09-11 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | * | | | | | | | | | | | | | | | | | Fix Typo in Doc for `Set Parsing Explicit` | staffehn | 2017-09-08 | |
| |_|_|_|_|/ / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | | * | Normalizing universes before performing term comparison. | Pierre-Marie Pédrot | 2017-09-08 | |
| | | | | | | | | | | | | | | | | | | | | * | Using EConstr equality check in unification. | Pierre-Marie Pédrot | 2017-09-08 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | ||||
| | | | | * | | | | | | | | | | | | | | | | 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 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |