aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-25Update changelogPierre Roux
2020-03-25Nicer printing for decimal constants in QPierre Roux
Print 1.5 as 1.5 and not 15e-1. We choose the shortest representation with tie break to the dot notation (0.01 rather than 1e-3). The printing remains injective, i.e. 12/10 is not mixed with 120/100, the first being printed as 1.2 and the last as 1.20.
2020-03-25Nicer printing for decimal constants in RPierre Roux
Print 1.5 as 1.5 and not 15e-1. We choose the shortest representation with tie break to the dot notation (0.01 rather than 1e-3). The printing remains injective, i.e. 12*10^2 is printed 12e2 in order not to mix it with 1200 and 12/10^1 is not mixed with 120/10^2, the first being printed as 1.2 and the last as 1.20.
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-24Run ocamlformat on modified ml / mli files in pre-commit hook.Théo Zimmermann
Thanks to `.ocamlformat-ignore`, we can call ocamlformat blindly but only the non-ignored files will be affected. Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-03-24“auto with zarith”: use “lia” rather than “omega”Vincent Laporte
2020-03-24[stdlib] Do not rely on failing “auto”Vincent Laporte
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-23Fix levels of `<=?` and `<?` in the stdlibJason Gross
They were defined at level 70, no associativity in all but three places, where they were instead declared at level 35. Fixes #11890
2020-03-23[ci] add metacoqMatthieu Sozeau
2020-03-23Sorting: Swap the names of Sorted_sort and LocallySorted_sortLysxia
2020-03-23Merge PR #11888: Fix broken links in prodn:: in docThéo Zimmermann
Reviewed-by: Zimmi48
2020-03-23s/magicaly/magically/Jason Gross
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.
2020-03-21Reorder the load/require cmd-options and set/unset cmd-optionsLasse Blaauwbroek
Make sure that all initial load vernaculars that were specified on the command line are executed before processing the options set through -set on the command line. The reason for this is that the load vernacular options can load plugins that define new Goptions. If these plugins are not loaded before the -set flags are processed, then Goptions will emit a warning that the options of that plugin don't exist and ignore the flag.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 23:20:56 +0000