| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-27 | Merge PR #6494: Remove legacy Value.normalize function. | Maxime Dénès | |
| 2017-12-27 | Merge PR #6289: Remove unused boolean from cl_context field of ↵ | Maxime Dénès | |
| Typeclasses.typeclass | |||
| 2017-12-27 | Merge PR #6473: Fix warning about shadowing a global name. | Maxime Dénès | |
| 2017-12-26 | [ide] [doc] Document tweak to Query call. | Emilio Jesus Gallego Arias | |
| 2017-12-26 | Fix overlay selection for Circle CI. | Gaëtan Gilbert | |
| 2017-12-26 | Delete old overlays (leaving example) | Gaëtan Gilbert | |
| 2017-12-24 | Check the whole string given by md5sum.ml | Jacques-Pascal Deplaix | |
| 2017-12-24 | Create pull request template. | Théo Zimmermann | |
| 2017-12-24 | Update backport script for more control. | Théo Zimmermann | |
| 2017-12-23 | Replace md5sum/md5 calls by an OCaml program | Jacques-Pascal Deplaix | |
| 2017-12-23 | [api] Also deprecate constructors of Decl_kinds. | Emilio Jesus Gallego Arias | |
| Unfortunately OCaml doesn't deprecate the constructors of a type when the type alias is deprecated. In this case it means that we don't get rid of the kernel dependency unless we deprecate the constructors too. | |||
| 2017-12-23 | [flags] Move global time flag into an attribute. | Emilio Jesus Gallego Arias | |
| One less global flag. | |||
| 2017-12-23 | [lib] Split auxiliary libraries into Coq-specific and general. | Emilio Jesus Gallego Arias | |
| Up to this point the `lib` directory contained two different library archives, `clib.cma` and `lib.cma`, which a rough splitting between Coq-specific libraries and general-purpose ones. We know split the directory in two, as to make the distinction clear: - `clib`: contains libraries that are not Coq specific and implement common data structures and programming patterns. These libraries could be eventually replace with external dependencies and the rest of the code base wouldn't notice much. - `lib`: contains Coq-specific common libraries in widespread use along the codebase, but that are not considered part of other components. Examples are printing, error handling, or flags. In some cases we have coupling due to utility files depending on Coq specific flags, however this commit doesn't modify any files, but only moves them around, further cleanup is welcome, as indeed a few files in `lib` should likely be placed in `clib`. Also note that `Deque` is not used ATM. | |||
| 2017-12-23 | Registering a printing handler in coq_makefile. | Hugo Herbelin | |
| This allows to fix the non-printing of error messages produced when parsing arguments. | |||
| 2017-12-23 | Forbidding -o and -f in input file of coq_makefile. | Hugo Herbelin | |
| This was apparently either silently doing nothing or failing. | |||
| 2017-12-23 | Removing failure of coq_makefile on no arguments. | Hugo Herbelin | |
| Nevertheless making option -o of coq_makefile recommended as discussed in PR#6040. This is one way to resolve the inconsistency with the usage which says that all arguments are optional. | |||
| 2017-12-22 | Add printers to dev/db | Gaëtan Gilbert | |
| 2017-12-22 | Reorder dev/db | Gaëtan Gilbert | |
| 2017-12-22 | Cleanup top_printers.mli | Gaëtan Gilbert | |
| 2017-12-22 | Cleanup debug printers a bit, add generated mli. | Gaëtan Gilbert | |
| 2017-12-22 | Merge PR #6465: Gitlab touchup | Maxime Dénès | |
| 2017-12-22 | Merge PR #6469: No universe constraints in Let definitions | Maxime Dénès | |
| 2017-12-22 | Merge PR #6318: Separate vernac controls and regular commands. | Maxime Dénès | |
| 2017-12-22 | Remove syntax for classification in TACTIC EXTEND. | Maxime Dénès | |
| It was left ignored after 8089dc960c9e8caf778907fd87be48d77b066433. | |||
| 2017-12-22 | Remove legacy Value.normalize function. | Maxime Dénès | |
| It was the identity. | |||
| 2017-12-22 | Merge PR #6484: Update README and CONTRIBUTING to mention the wiki and FAQ. | Maxime Dénès | |
| 2017-12-22 | Merge PR #6485: Fix badges. | Maxime Dénès | |
| 2017-12-22 | Merge PR #6445: [stm] [ide protocol] Allow to include several commands on query. | Maxime Dénès | |
| 2017-12-22 | Merge PR #6222: Share computation of unifiable evars | Maxime Dénès | |
| 2017-12-21 | Merge code paths in interp_definition and cleanup a bit. | Gaëtan Gilbert | |
| 2017-12-21 | Fix badges. | Théo Zimmermann | |
| 2017-12-21 | Update README and CONTRIBUTING to mention the wiki and FAQ. | Théo Zimmermann | |
| 2017-12-21 | Merge PR #6474: Fix CI with parallel make (messed up dependencies) | Maxime Dénès | |
| 2017-12-21 | Fix CI with parallel make (messed up dependencies) | Gaëtan Gilbert | |
| When invoking through Makefile we always rebuild dependencies. To skip dependencies, invoke ci-wrapper directly. We make Circle CI do this. In order to properly support invoking ci-wrapper directly we replace "make" in ci-common by a bash function which adds -j to the make invocation outside submakes. We also set TIMED in the ci-wrapper. | |||
| 2017-12-20 | Separate vernac controls and regular commands. | Maxime Dénès | |
| Virtually all classifications of vernacular commands (the STM classifier, "filtered commands", "navigation commands", etc.) were broken in presence of control vernaculars like Time, Timeout, Fail. Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac Debug in CoqIDE. This change introduces a type separation between vernacular controls and vernacular commands, together with an "under_control" combinator. | |||
| 2017-12-20 | Merge PR #6377: Removal of the FAQ LaTex document. | Maxime Dénès | |
| 2017-12-20 | Merge PR #6470: Fix typo in the refman. | Maxime Dénès | |
| 2017-12-20 | Merge PR #6449: Let definitions must not contain side-effects when reaching ↵ | Maxime Dénès | |
| the kernel. | |||
| 2017-12-20 | Merge PR #6468: Fix order of let-in representation comment. | Maxime Dénès | |
| 2017-12-20 | Merge PR #6471: Fix ltacprof_abstract (I think because of #6411 parallel merge). | Maxime Dénès | |
| 2017-12-20 | Merge PR #6234: Make the micromega extraction check a regular output test. | Maxime Dénès | |
| 2017-12-19 | Fix warning about shadowing a global name. | Gaëtan Gilbert | |
| 2017-12-19 | Fix ltacprof_abstract (I think because of #6411 parallel merge). | Gaëtan Gilbert | |
| 2017-12-19 | Fix typo in the refman. | Théo Zimmermann | |
| 2017-12-19 | Let definitions do not create new universe constraints. | Pierre-Marie Pédrot | |
| We force the upper layers to extrude the universe constraints before sending it to the kernel. This simplifies the suspicious handling of polymorphic constraints for section-local definitions. | |||
| 2017-12-19 | Merge PR #6400: Circle CI | Maxime Dénès | |
| 2017-12-19 | Specific type for section definition entries. | Pierre-Marie Pédrot | |
| This allows to statically ensure well-formedness properties. | |||
| 2017-12-19 | Fix order of let-in representation comment. | Jasper Hugunin | |
| The comment had the type and value of the let-in swapped, which contradicted the listed types. | |||
| 2017-12-18 | Gitlab: don't ./configure in documentation job | Gaëtan Gilbert | |
| The config/Makefile is carried over by artefacts. | |||
| 2017-12-18 | Merge PR #6436: Fix #5368: Canonical structure unification fails. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |