aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Recdef do now a Require Export FunInd (better compat)Gravatar Pierre Letouzey2017-06-14
|
* Grammar hacks to get nice errors about non-loaded plugins (extr,recdef)Gravatar Pierre Letouzey2017-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.mliGravatar Pierre Letouzey2017-06-14
|
* Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-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 ↵Gravatar Pierre Letouzey2017-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.Gravatar Maxime Dénès2017-06-14
|
* Merge PR#498: Bignums as a separate opam packageGravatar Maxime Dénès2017-06-14
|\
* | Makefile.build: do *not* build PLUGINSCMO by default (followup of PR #709)Gravatar Pierre Letouzey2017-06-13
| |
* | Merge PR#385: Equality of sigma typesGravatar Maxime Dénès2017-06-13
|\ \
* \ \ Merge PR#766: Fix ocamldebug for the APIGravatar Maxime Dénès2017-06-13
|\ \ \
* \ \ \ Merge PR#714: Print feature Proof-of-Concept (episode 2)Gravatar Maxime Dénès2017-06-13
|\ \ \ \
| | | | * [travis] overlay for cornGravatar Pierre Letouzey2017-06-13
| | | | |
| | | | * [travis] extra test ci-bignums (+factorize other scripts)Gravatar Pierre Letouzey2017-06-13
| | | | |
| | | | * [travis] overlay + extra deps for math-classes (and formal-topology)Gravatar Pierre Letouzey2017-06-13
| | | | |
* | | | | Merge PR#757: Better sectioning on travis log printing in test-suiteGravatar Maxime Dénès2017-06-13
|\ \ \ \ \
| | | | | * [travis] adapt CoLoR compilation to depend on the bignum packageGravatar Pierre Letouzey2017-06-13
| | | | | |
| | | | | * BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-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 .gitignoreGravatar Maxime Dénès2017-06-13
|\ \ \ \ \
* \ \ \ \ \ Merge PR#764: Point ci-hott at a newer version of HoTTGravatar Maxime Dénès2017-06-13
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#772: Store plugins/micromega/micromega.{ml,mli} files in the ↵Gravatar Maxime Dénès2017-06-13
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | repository. Try to generate them later.
| * | | | | | | Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to ↵Gravatar Matej Košík2017-06-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | generate them later.
* | | | | | | | Merge PR#715: Add coq-dpdgraph ciGravatar Maxime Dénès2017-06-12
|\ \ \ \ \ \ \ \ | |/ / / / / / / |/| | | | | | |
* | | | | | | | Merge PR#709: Bytecode compilation apart from 'make world', againGravatar Maxime Dénès2017-06-12
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#718: API cleanup: aliasesGravatar Maxime Dénès2017-06-12
|\ \ \ \ \ \ \ \ \
* | | | | | | | | | Temporary overlay, waiting for upstream PR merges.Gravatar Maxime Dénès2017-06-12
| | | | | | | | | |
* | | | | | | | | | Merge PR#707: add support for "-bypass-API" argument to "coq_makefile"Gravatar Maxime Dénès2017-06-12
|\ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | add overlaysGravatar Matej Košík2017-06-12
| | | | | | | | | | |
| * | | | | | | | | | Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-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 XGravatar Maxime Denes2017-06-12
| | | | | | | | | | |
| | | | | | | | | * | Fix ocamldebug for the APIGravatar Gaëtan Gilbert2017-06-12
| | |_|_|_|_|_|_|/ / | |/| | | | | | | |
| | | | | * | | | | Point ci-hott at a newer version of HoTTGravatar Jason Gross2017-06-11
| | |_|_|/ / / / / | |/| | | | | | |
| * | | | | | | | Remove remaining vo.itarget files (obsolete since PR #499)Gravatar Pierre Letouzey2017-06-10
| | | | | | | | |
| | | | | | * | | Fix Travis sectioningGravatar Jason Gross2017-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.Gravatar Matej Košík2017-06-10
| |/ / / / / / / |/| | | | | | |
| | | | | * | | Better sectioning on travis log printing in test-suiteGravatar Jason Gross2017-06-09
| | |_|_|/ / / | |/| | | | |
| * | | | | | Makefile.common: remove an obsolete comment after PR#499Gravatar Pierre Letouzey2017-06-09
| | | | | | |
| | | * | | | Mirror dpdgraph's travis test more accuratelyGravatar Jason Gross2017-06-08
| | | | | | |
| | | * | | | Remove coq-dpdgraph overlayGravatar Jason Gross2017-06-08
| | | | | | |
| * | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|/| | | | | |
* | | | | | | Remove overlay.Gravatar Maxime Dénès2017-06-08
| | | | | | |
* | | | | | | Merge PR#652: Put all plugins behind an "API".Gravatar Maxime Dénès2017-06-08
|\ \ \ \ \ \ \
| | | | | * | | Update .gitignoreGravatar Jason Gross2017-06-07
| |_|_|_|/ / / |/| | | | | |
| * | | | | | add overlaysGravatar Matej Košík2017-06-07
| | | | | | |
| * | | | | | Put "ssreflect" behind "API".Gravatar Matej Košík2017-06-07
| | | | | | |
| * | | | | | Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
|/ / / / / /
* | | | | | Merge PR#698: Trunk miscGravatar Maxime Dénès2017-06-07
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#717: [proof] Deprecate "proof mode" APIGravatar Maxime Dénès2017-06-07
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#669: Ssr mergeGravatar Maxime Dénès2017-06-07
|\ \ \ \ \ \ \ \
| * | | | | | | | Overlay.Gravatar Maxime Dénès2017-06-06
| | | | | | | | |
| * | | | | | | | Merge the ssr plugin.Gravatar Maxime Dénès2017-06-06
|/ / / / / / / /
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 21:25:07 +0000