aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-06-14Recdef do now a Require Export FunInd (better compat)Pierre Letouzey
2017-06-14Grammar hacks to get nice errors about non-loaded plugins (extr,recdef)Pierre Letouzey
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.
2017-06-14API: exports Mltop.module_is_known to both API.mli and grammar_API.mliPierre Letouzey
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
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.
2017-06-14Makefile.build : cleanup now that micromega.ml isn't generated + sync check ↵Pierre Letouzey
of this file There is now a warning if the content of micromega.ml isn't what MExtraction.v would produce.
2017-06-14Temporary overlays for bignums.Maxime Dénès
2017-06-14Merge PR#498: Bignums as a separate opam packageMaxime Dénès
2017-06-13Makefile.build: do *not* build PLUGINSCMO by default (followup of PR #709)Pierre Letouzey
2017-06-13Merge PR#385: Equality of sigma typesMaxime Dénès
2017-06-13Merge PR#766: Fix ocamldebug for the APIMaxime Dénès
2017-06-13Merge PR#714: Print feature Proof-of-Concept (episode 2)Maxime Dénès
2017-06-13[travis] overlay for cornPierre 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-13Merge PR#757: Better sectioning on travis log printing in test-suiteMaxime Dénès
2017-06-13[travis] adapt CoLoR compilation to depend on the bignum packagePierre Letouzey
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
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.
2017-06-13Merge PR#743: Update .gitignoreMaxime Dénès
2017-06-13Merge PR#764: Point ci-hott at a newer version of HoTTMaxime Dénès
2017-06-13Merge PR#772: Store plugins/micromega/micromega.{ml,mli} files in the ↵Maxime Dénès
repository. Try to generate them later.
2017-06-12Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to ↵Matej Košík
generate them later.
2017-06-12Merge PR#715: Add coq-dpdgraph ciMaxime Dénès
2017-06-12Merge PR#709: Bytecode compilation apart from 'make world', againMaxime Dénès
2017-06-12Merge PR#718: API cleanup: aliasesMaxime Dénès
2017-06-12Temporary overlay, waiting for upstream PR merges.Maxime Dénès
2017-06-12Merge PR#707: add support for "-bypass-API" argument to "coq_makefile"Maxime Dénès
2017-06-12add overlaysMatej Košík
2017-06-12Add support for "-bypass-API" argument of "coq_makefile"Matej Košík
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
2017-06-12make test-suite/save-logs.sh usable also on old MacOS XMaxime Denes
2017-06-12Fix ocamldebug for the APIGaëtan Gilbert
2017-06-11Point ci-hott at a newer version of HoTTJason Gross
2017-06-10Remove remaining vo.itarget files (obsolete since PR #499)Pierre Letouzey
2017-06-10Fix Travis sectioningJason Gross
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?
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-09Better sectioning on travis log printing in test-suiteJason Gross
2017-06-09Makefile.common: remove an obsolete comment after PR#499Pierre Letouzey
2017-06-08Mirror dpdgraph's travis test more accuratelyJason Gross
2017-06-08Remove coq-dpdgraph overlayJason Gross
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-08Remove overlay.Maxime Dénès
2017-06-08Merge PR#652: Put all plugins behind an "API".Maxime Dénès
2017-06-07Update .gitignoreJason Gross
2017-06-07add overlaysMatej Košík
2017-06-07Put "ssreflect" behind "API".Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-07Merge PR#698: Trunk miscMaxime Dénès
2017-06-07Merge PR#717: [proof] Deprecate "proof mode" APIMaxime Dénès
2017-06-07Merge PR#669: Ssr mergeMaxime Dénès
2017-06-06Overlay.Maxime Dénès
2017-06-06Merge the ssr plugin.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 01:57:33 +0000