aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-08-31prim notations backtrackable, their declarations now in two parts (API change)Pierre Letouzey
The first part (e.g. register_bignumeral_interpretation) deals only with the interp/uninterp closures. It should typically be done as a side effect during a syntax plugin loading. No prim notation are active yet after this phase. The second part (enable_prim_token_interpretation) activates the prim notation. It is now correctly talking to Summary and to the LibStack. To avoid "phantom" objects in libstack after a mere Require, this second part should be done inside a Mltop.declare_cache_obj The link between the two parts is a prim_token_uid (a string), which should be unique for each primitive notation. When this primitive notation is specific to a scope, the scope_name could be used as uid. Btw, the list of "patterns" for detecting when an uninterpreter should be considered is now restricted to a list of global_reference (inductive constructors, or injection functions such as IZR). The earlier API was accepting a glob_constr list, but was actually only working well for global_reference. A minimal compatibility is provided (declare_numeral_interpreter), but is discouraged, since it is known to store uncessary objects in the libstack.
2018-08-31Prelude : update the comment about ML plugins loaded by InitPierre Letouzey
2018-08-31Extraargs: avoid two token declarations to appear in all .voPierre Letouzey
Without this, the library segment of all .vo except Notations.vo starts with two TOKEN objects (declaration of tokens "->" and "<-"). This is due to side effects creating these objects during the dynlink of ltac_plugin.cmxs, more precisely the two Metasyntax.add_token_obj in Extraargs. It's quite cleaner to register these two side effects via Mltop.declare_cache_obj, so that the two objects only live in Notations.vo, and are loaded from there.
2018-08-31Tacenv: minor code cleanupPierre Letouzey
2018-08-31Notation: remove support for prim tokens denoting inductive types in "return"Pierre Letouzey
This is prim token notations for inductive *types*, not values. So we're speaking of a scope where 0 is the type nat, 1 is the type bool, etc. To my knowledge, this feature hasn't ever been used, and is very unlikely to be used ever, so let's clean the code a bit by removing it.
2018-08-31Notation: avoid one intermediate (unit -> ...)Pierre Letouzey
2018-08-31Notation: no more chains of prim_token_interpreterPierre Letouzey
This cleanup prepares for forthcoming synchronization of prim_token_interpreter wrt to Summary. These chains of prim_token_interpreter were anyway never used, only one interpreter was declared per numeral scope. After sync wrt Summary, we'll anyway be able to backtrack to a previous interpreter.
2018-09-01Merge PR #8348: Download tarball instead of cloning external projects.Emilio Jesus Gallego Arias
2018-08-31Merge PR #8346: Clean-up Travis folds.Gaëtan Gilbert
2018-08-31Merge PR #8351: [ci] [docker] Update base Dune version.Gaëtan Gilbert
2018-08-31Merge PR #8170: Don't index names starting with `_` in docsThéo Zimmermann
2018-08-31Merge PR #8219: Refman consistency checkThéo Zimmermann
2018-08-31Download tarball instead of cloning external projects (when $CI is set).Théo Zimmermann
This allows to use fixed commits and not just branches or tags. We keep using git clone when $FORCE_GIT is set (for projects on gforge.inria.fr and projects pulling dependencies through git submodules). fiat-parsers also calls git submodule, but inside its own Makefile.
2018-08-31Merge PR #8368: [ci] Fix QuickChick by adding new simple-io dependency.Gaëtan Gilbert
2018-08-31[ci] Fix QuickChick by adding new simple-io dependency.Théo Zimmermann
2018-08-31Fixed the seealso directive in a few places.Zeimer
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: ↵Zeimer
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
2018-08-30[ci] [docker] Update Dune and Elpi versions.Emilio Jesus Gallego Arias
We'd like to use `(lang 1.1)` features. Elpi needs update as recent `ppx_tools_versioned` changes broke it.
2018-08-30Merge PR #8354: Move CHANGES entry for #8167 to 8.8.2 sectionThéo Zimmermann
2018-08-30Merge PR #8349: Mention dev/doc/critical-bugs in CONTRIBUTINGThéo Zimmermann
2018-08-30Merge PR #8292: Create SPHINXWARNERROR variable to control Sphinx "warn as ↵Théo Zimmermann
error" argument in make
2018-08-29Merge PR #8353: [sphinx] Fix timeout issue by splitting imports.Clément Pit-Claudel
2018-08-29Merge PR #8345: Add index for focusing braces.Clément Pit-Claudel
2018-08-29Create SPHINXWARNERROR variable that controls whether the SphinxJim Fehrle
"treat errors as warnings" flag (-W) is applied. "1" or undefined includes the flag, other values or undefined omit it. Removed the "-warn-error" parameter to configure. "-profile XXX" will no longer cause these flags to be used.
2018-08-29Move CHANGES entry for #8167 to 8.8.2 sectionJason Gross
As per https://github.com/coq/coq/pull/8167#issuecomment-416929865
2018-08-29Move mention of dev/doc/critical-bugs to CONTRIBUTINGJason Gross
As per https://github.com/coq/coq/pull/8349#pullrequestreview-150456919
2018-08-29Mention dev/doc/critical-bugs in the PR templateJason Gross
2018-08-29[sphinx] Fix timeout issue by splitting imports.Théo Zimmermann
2018-08-29Merge PR #8274: Restore previous printing filtering; always reprint the ↵Emilio Jesus Gallego Arias
context after "Set Diffs"
2018-08-29Merge PR #8313: [ci-fiat-crypto] Test extractionEmilio Jesus Gallego Arias
2018-08-29Merge PR #8350: Fix typo in comment, sollicited --> solicited.Emilio Jesus Gallego Arias
2018-08-29Merge PR #8282: [coq_makefile] print all options (Fix #7529)Théo Zimmermann
2018-08-29Merge PR #8167: Fix ordering of before/after in print-pretty-timed-*Enrico Tassi
2018-08-29Merge PR #8340: Put camldevfiles targets in MakefileEnrico Tassi
2018-08-28Merge PR #8334: Fix a casing problem noticed by Lars Dölle on Coq-Club.Clément Pit-Claudel
2018-08-28Fix typo in comment, sollicited --> solicited.Nick Lewycky
2018-08-28[ci-fiat-crypto] Build c-filesJason Gross
This tests the outputs of extraction, to some extent.
2018-08-28Merge PR #8135: Sphinx fixing of the beginning of the Tactics chapter.Clément Pit-Claudel
2018-08-28Merge PR #8281: Trivial Sphinx fix in doc.Clément Pit-Claudel
2018-08-28Clean-up Travis folds.Théo Zimmermann
This has become mostly garbage since GitLab CI became our main CI platform.
2018-08-28Add index for focusing braces.Théo Zimmermann
And fix wrong indentation.
2018-08-28Merge PR #8333: Fix URIs in the configuration scriptEmilio Jesus Gallego Arias
2018-08-28Put camldevfiles targets in MakefileGaëtan Gilbert
There's no need to build dependencies for it.
2018-08-28Merge PR #8112: Add support for focusing on named goals using brackets.Pierre-Marie Pédrot
2018-08-27Update test-suite for focusing on named goals.Théo Zimmermann
2018-08-27Document focusing on named goals.Théo Zimmermann
2018-08-27Add support for focusing on named goals using brackets.Théo Zimmermann
2018-08-27Merge PR #8312: Split up fiat-crypto CI into two targetsGaëtan Gilbert
2018-08-27Merge PR #8260: Tweak diff options in CoqIDEPierre-Marie Pédrot
2018-08-27Fix a casing problem noticed by Lars Dölle on Coq-Club.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 21:05:42 +0000