Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Grammar hacks to get nice errors about non-loaded plugins (extr,recdef) | Pierre Letouzey | 2017-06-14 |
| | | | | | | | | | | | | | | Since previous commit, some plugins are not loaded initially anymore : extraction, funind. To ease this transition toward a mandatory Require, we hack here the vernac grammar in order to get customized error messages telling what to Require instead of the dreadful "Illegal begin of vernac". Normally, these fake grammar entries are overloaded later by the grammar extensions in these plugins. This code is meant to be removed in a few releases, when this transition is considered finished. NB : In a first attempt, a similar trick was tried in g_tactics.ml4 to provide customized error message for "functional induction" and "functional inversion", but this was leading to anomalies. | ||
* | API: exports Mltop.module_is_known to both API.mli and grammar_API.mli | Pierre Letouzey | 2017-06-14 |
| | |||
* | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey | 2017-06-14 |
| | | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted. | ||
* | Makefile.build : cleanup now that micromega.ml isn't generated + sync check ↵ | Pierre Letouzey | 2017-06-14 |
| | | | | | | | of this file There is now a warning if the content of micromega.ml isn't what MExtraction.v would produce. | ||
* | Temporary overlays for bignums. | Maxime Dénès | 2017-06-14 |
| | |||
* | Merge PR#498: Bignums as a separate opam package | Maxime Dénès | 2017-06-14 |
|\ | |||
* | | Makefile.build: do *not* build PLUGINSCMO by default (followup of PR #709) | Pierre Letouzey | 2017-06-13 |
| | | |||
* | | Merge PR#385: Equality of sigma types | Maxime Dénès | 2017-06-13 |
|\ \ | |||
* \ \ | Merge PR#766: Fix ocamldebug for the API | Maxime Dénès | 2017-06-13 |
|\ \ \ | |||
* \ \ \ | Merge PR#714: Print feature Proof-of-Concept (episode 2) | Maxime Dénès | 2017-06-13 |
|\ \ \ \ | |||
| | | | * | [travis] overlay for corn | Pierre Letouzey | 2017-06-13 |
| | | | | | |||
| | | | * | [travis] extra test ci-bignums (+factorize other scripts) | Pierre Letouzey | 2017-06-13 |
| | | | | | |||
| | | | * | [travis] overlay + extra deps for math-classes (and formal-topology) | Pierre Letouzey | 2017-06-13 |
| | | | | | |||
* | | | | | Merge PR#757: Better sectioning on travis log printing in test-suite | Maxime Dénès | 2017-06-13 |
|\ \ \ \ \ | |||
| | | | | * | [travis] adapt CoLoR compilation to depend on the bignum package | Pierre Letouzey | 2017-06-13 |
| | | | | | | |||
| | | | | * | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey | 2017-06-13 |
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude. | ||
* | | | | | Merge PR#743: Update .gitignore | Maxime Dénès | 2017-06-13 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR#764: Point ci-hott at a newer version of HoTT | Maxime Dénès | 2017-06-13 |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR#772: Store plugins/micromega/micromega.{ml,mli} files in the ↵ | Maxime Dénès | 2017-06-13 |
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | repository. Try to generate them later. | ||
| * | | | | | | | Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to ↵ | Matej Košík | 2017-06-12 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | generate them later. | ||
* | | | | | | | | Merge PR#715: Add coq-dpdgraph ci | Maxime Dénès | 2017-06-12 |
|\ \ \ \ \ \ \ \ | |/ / / / / / / |/| | | | | | | | |||
* | | | | | | | | Merge PR#709: Bytecode compilation apart from 'make world', again | Maxime Dénès | 2017-06-12 |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR#718: API cleanup: aliases | Maxime Dénès | 2017-06-12 |
|\ \ \ \ \ \ \ \ \ | |||
* | | | | | | | | | | Temporary overlay, waiting for upstream PR merges. | Maxime Dénès | 2017-06-12 |
| | | | | | | | | | | |||
* | | | | | | | | | | Merge PR#707: add support for "-bypass-API" argument to "coq_makefile" | Maxime Dénès | 2017-06-12 |
|\ \ \ \ \ \ \ \ \ \ | |||
| * | | | | | | | | | | add overlays | Matej Košík | 2017-06-12 |
| | | | | | | | | | | | |||
| * | | | | | | | | | | Add support for "-bypass-API" argument of "coq_makefile" | Matej Košík | 2017-06-12 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac | ||
| * | | | | | | | | | | make test-suite/save-logs.sh usable also on old MacOS X | Maxime Denes | 2017-06-12 |
| | | | | | | | | | | | |||
| | | | | | | | | * | | Fix ocamldebug for the API | Gaëtan Gilbert | 2017-06-12 |
| | |_|_|_|_|_|_|/ / | |/| | | | | | | | | |||
| | | | | * | | | | | Point ci-hott at a newer version of HoTT | Jason Gross | 2017-06-11 |
| | |_|_|/ / / / / | |/| | | | | | | | |||
| * | | | | | | | | Remove remaining vo.itarget files (obsolete since PR #499) | Pierre Letouzey | 2017-06-10 |
| | | | | | | | | | |||
| | | | | | * | | | Fix Travis sectioning | Jason Gross | 2017-06-10 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It drops anything after a `/`, so we change all `/`s into `.`. There must be a better way to do this that doesn't involve so much bash hackery, right? | ||
| | * | | | | | | | Remove (useless) aliases from the API. | Matej Košík | 2017-06-10 |
| |/ / / / / / / |/| | | | | | | | |||
| | | | | * | | | Better sectioning on travis log printing in test-suite | Jason Gross | 2017-06-09 |
| | |_|_|/ / / | |/| | | | | | |||
| * | | | | | | Makefile.common: remove an obsolete comment after PR#499 | Pierre Letouzey | 2017-06-09 |
| | | | | | | | |||
| | | * | | | | Mirror dpdgraph's travis test more accurately | Jason Gross | 2017-06-08 |
| | | | | | | | |||
| | | * | | | | Remove coq-dpdgraph overlay | Jason Gross | 2017-06-08 |
| | | | | | | | |||
| * | | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-06-08 |
|/| | | | | | | |||
* | | | | | | | Remove overlay. | Maxime Dénès | 2017-06-08 |
| | | | | | | | |||
* | | | | | | | Merge PR#652: Put all plugins behind an "API". | Maxime Dénès | 2017-06-08 |
|\ \ \ \ \ \ \ | |||
| | | | | * | | | Update .gitignore | Jason Gross | 2017-06-07 |
| |_|_|_|/ / / |/| | | | | | | |||
| * | | | | | | add overlays | Matej Košík | 2017-06-07 |
| | | | | | | | |||
| * | | | | | | Put "ssreflect" behind "API". | Matej Košík | 2017-06-07 |
| | | | | | | | |||
| * | | | | | | Put all plugins behind an "API". | Matej Kosik | 2017-06-07 |
|/ / / / / / | |||
* | | | | | | Merge PR#698: Trunk misc | Maxime Dénès | 2017-06-07 |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR#717: [proof] Deprecate "proof mode" API | Maxime Dénès | 2017-06-07 |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR#669: Ssr merge | Maxime Dénès | 2017-06-07 |
|\ \ \ \ \ \ \ \ | |||
| * | | | | | | | | Overlay. | Maxime Dénès | 2017-06-06 |
| | | | | | | | | | |||
| * | | | | | | | | Merge the ssr plugin. | Maxime Dénès | 2017-06-06 |
|/ / / / / / / / | |||
* | | | | | | | | Remove some overlays. | Maxime Dénès | 2017-06-06 |
| | | | | | | | |