aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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.
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.
2020-03-20Fix the computation of recursive principles with let-bindings.Pierre-Marie Pédrot
We use a more robust implementation that does not assume that the type of the inductive is in ζ-normal form. This code path is not exercised, because due to the kernel typing algorithm, let-bindings in the type of a recursor are expanded away.
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-03-20Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yesEnrico Tassi
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares
2020-03-20Merge PR #11847: Properly thread let-bindings in Funind principle construction.Pierre Courtieu
Reviewed-by: Matafou
2020-03-20Merge PR #11778: [ocamformat] Update to 0.13.0Théo Zimmermann
Reviewed-by: Zimmi48
2020-03-20Build and install refman with Dune.Théo Zimmermann
2020-03-20Merge PR #11857: Remove calls to structural equality in MicromegaVincent Laporte
Reviewed-by: vbgl
2020-03-19Merge PR #11601: [refman] Move chapters into new structure.Clément Pit-Claudel
Reviewed-by: jfehrle
2020-03-19[ocamformat] Update to 0.13.0Emilio Jesus Gallego Arias
We include the `version=0.13.0` field that should help users not to use the wrong version. `disable=true` still seems a noop with `dune`. There are some minor changes in the way comments are formatted; I'm unsure if this is due to the `wrap-comments` option; as always; tweaks to the config are most welcome.
2020-03-19[obligations] Step towards more structured handling of remaining obligations.Emilio Jesus Gallego Arias
There is a lot of check overhead in the code, we will try to provide a more convenient API for manipulation of remaining obligations.
2020-03-19[obligations] Refactor some common code on save pathEmilio Jesus Gallego Arias
Both the interactive and non-interactive save path share some internal table update code.
2020-03-19[obligations] More progress towards unification of the save pathEmilio Jesus Gallego Arias
We make internal types `private` as an step towards the unification of the save path with the rest of the system. In particular, this is allow us to guarantee invariants w.r.t. external users as the large majority of fields are always constant. This will also enable at some point a common creation of proof entry with the rest of the system.
2020-03-19[comFixpoint] Cleanup on opens prior to fix unificationEmilio Jesus Gallego Arias
2020-03-19[proof] Remove duplicated poly field in Proof_global.tEmilio Jesus Gallego Arias
2020-03-19[pfedit] Labelize sign parameterEmilio Jesus Gallego Arias
2020-03-19[declare] Remaining bits on the consistency of UState.t namingEmilio Jesus Gallego Arias
2020-03-19[vernac] Make local exception localEmilio Jesus Gallego Arias
2020-03-19[comFixpoing] Refactor hybrid interactive command modalityEmilio Jesus Gallego Arias
2020-03-19[lemmas] Fix comment on public APIEmilio Jesus Gallego Arias
After we moved `start_lemma_com` to `vernacentries` the comment on `start_lemma_with_initialization` needs update.
2020-03-19[lemma] Remove double normalization of typesEmilio Jesus Gallego Arias
It should be safe now after previous refactoring in lemmas.
2020-03-19[declare/lemmas] Make inference hook exception-freeEmilio Jesus Gallego Arias
This is a step towards cleanup of the `start` lemma path.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:06:25 +0000