aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-03-25[parsing] Move `coq_parsable` custom logic to Grammar.Emilio Jesus Gallego Arias
Latest refactorings allow us to make the signature Coq parser a standard `Grammar.S` one; the only bit needed is to provide the extra capabilities to the `Lexer` signature w.r.t. to comments state. The handling of Lexer state is still a bit ad-hoc, in particular it is global whereas it should be fully attached to the parsable. This may work ok in batch mode but the current behavior may be buggy in the interactive context. This PR doesn't solve that but it is a step towards a more functional solution.
2020-03-25[parsing] Remove redundant interfaces from PcoqEmilio Jesus Gallego Arias
There is not need to re-export Gramlib's API in a non-structured way anymore. We thus expose the core Gramlib interface to users and remove redundant functions. A question about whether to move more parts of the API to `Gramlib` is still open, as well as on naming.
2020-03-25[parsing] Remove unneeded `Extend.entry` type.Emilio Jesus Gallego Arias
This is not needed anymore after the unification.
2020-03-25[parsing] Remove extend AST in favor of gramlib constructorsEmilio Jesus Gallego Arias
We remove Coq's wrapper over gramlib's grammar constructors.
2020-03-25[parsing] Make grammar rules private.Emilio Jesus Gallego Arias
After the gramlib merge and the type-safe interface added to it, the grammar extension type is redundant; we thus make it private as a first step on consolidating it with the one in gramlib's.
2020-03-25[parsing] Make grammar extension type private.Emilio Jesus Gallego Arias
After the gramlib merge and the type-safe interface added to it, the grammar extension type is redundant; we thus make it private as a first step on consolidating it with the one in gramlib's.
2020-03-25[gitlab] Increase flambda stack size.Emilio Jesus Gallego Arias
See https://github.com/ocaml/ocaml/issues/7842
2020-03-25Merge PR #11898: Switch opam file to makeEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-03-25Merge PR #11705: Convert Gallina Extensions chapter to use prodnsThéo Zimmermann
Ack-by: Zimmi48
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-25Merge PR #11785: [proof] consolidation of mutual definition declaration pathGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: herbelin Reviewed-by: ppedrot
2020-03-25Merge PR #11875: Fix deploy of refman following #11855.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: ejgallego
2020-03-25Add a specific opam file to build te docker imagePierre Roux
The Docker image coqorg/coq:dev is currently built using the OPAM file coq.opam. Since this file is used for develoment purpose, it would be better to use a more stable one for building the docker images. The OPAM option "--locked=docker" will then be used in the opam pin command when building the docker image to use the new coq.opam.docker file. The new file builds Coq using make, this is temporary and could be reverted to dune once it supports "-native-compiler yes".
2020-03-25[declare] make restrict_ucontext an optional parameter.Emilio Jesus Gallego Arias
The current API does just exist as a workaround for a bug.
2020-03-25[lemmas] Use direct-style for mutual lemma declaration.Emilio Jesus Gallego Arias
Steps towards unification with `DeclareDef` API.
2020-03-25[lemmas] Use direct-style for variable declaration.Emilio Jesus Gallego Arias
Steps towards unification with `DeclareDef` API.
2020-03-25[proof] [mutual] Factorize mutual per-entry informationEmilio Jesus Gallego Arias
We move `Recthm` to `DeclareDef` so it is shared by interactive and direct fixpoint declaration. This is the last step before unifying both paths.
2020-03-25[proof] [mutual] Factorize universe handling.Emilio Jesus Gallego Arias
Note that we had to introduce a `restrict_ucontext` parameter to be faithful to the implementation in obligations, however this looks like a bug.
2020-03-25[proof] [mutual] Factorize mutual body construction.Emilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize notation declaration.Emilio Jesus Gallego Arias
2020-03-25[proof] Factorize call info message in mutual declarationsEmilio Jesus Gallego Arias
2020-03-25[proof] Start of mutual definition save refactoring.Emilio Jesus Gallego Arias
First commit of a series that will unify (and enforce) the handling of mutual constants. We will split this in several commits as to easy debugging / bisect in case of problems. In this first commit, we move the actual declare logic to a common place.
2020-03-24Merge PR #11703: Making of NumTok an API for numeralPierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: ppedrot Reviewed-by: proux01
2020-03-24Merge PR #11772: [obligations] Don't allocate libobjects for obligation info.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-24Merge PR #11826: [proof] Deprecate unused tacmach functions.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-24Merge PR #11858: Rename Retypeops -> RelevanceopsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-24Fix world and watch targets of Makefile.dune now that doc has install rules.Théo Zimmermann
2020-03-24Fix deploy of refman following #11855.Théo Zimmermann
2020-03-24Merge PR #11892: [refman] Fix caching, which was broken by the addition of ↵Théo Zimmermann
coq_config Reviewed-by: Zimmi48
2020-03-23Merge PR #9607: [ci] add metacoqGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: ejgallego
2020-03-23[refman] Fix caching, which was broken by the addition of coq_configClément Pit-Claudel
2020-03-23[ci] add metacoqMatthieu Sozeau
2020-03-23Merge PR #11888: Fix broken links in prodn:: in docThéo Zimmermann
Reviewed-by: Zimmi48
2020-03-23Merge PR #11867: Fix the computation of recursive principles with let-bindings.Enrico Tassi
Reviewed-by: gares
2020-03-23Merge PR #11442: Add module ZifyPow to avoid compatibility issue with 8.11.Frédéric Besson
Reviewed-by: fajb
2020-03-22Format hyperlink targets and link ids with the same nameJim Fehrle
(translate '_' to '-' consistently)
2020-03-22[obligations] Don't allocate libobjects for obligation info.Emilio Jesus Gallego Arias
Obligations/Program currently allocates a libobject object just to check that there are no obligations pending at the end of a section. I think this is not the right use case for libobject, thus we turn the check into an explicit one at the vernac level.
2020-03-22[obligations] Small cleanup for openEmilio Jesus Gallego Arias
2020-03-22Testing notations which are specific numerals.Hugo Herbelin
2020-03-22Adding support for parsing "+" sig in NumTok.Hugo Herbelin
Support in the parser needs yet to be added though.
2020-03-22Overlay for QuickChickHugo Herbelin
2020-03-22Adding a test for printing single characters.Hugo Herbelin
Originally from bedrock2.
2020-03-22Test-suite: Assume coqtop output is text even with non-printable characters.Hugo Herbelin
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
Four types of numerals are introduced: - positive natural numbers (may include "_", e.g. to separate thousands, and leading 0) - integer numbers (may start with a minus sign) - positive numbers with mantisse and signed exponent - signed numbers with mantisse and signed exponent In passing, we clarify that the lexer parses only positive numerals, but the numeral interpreters may accept signed numerals. Several improvements and fixes come from Pierre Roux. See https://github.com/coq/coq/pull/11703 for details. Thanks to him.
2020-03-22Adding bignat to parse positive numbers; bigint now includes negative ints.Hugo Herbelin
Warning: in notations, the name "bigint" actually meant "bignat". A clarification will eventually be needed.
2020-03-22Merge PR #11731: [proof] Miscellaneous refactoringsGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-03-22Merge PR #11851: Process command line load vernaculars before command line ↵Emilio Jesus Gallego Arias
Goptions Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2020-03-22Merge PR #11855: Build and install refman with Dune.Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2020-03-22[proof] Deprecate unused tacmach functions.Emilio Jesus Gallego Arias
2020-03-21Add module ZifyPow to avoid compatibility issue with 8.11.Théo Zimmermann
Also tweak the changelog entry to explain the difference.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 02:10:29 +0000