aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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-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.
2020-03-19[ci] Overlays for declare interface refactoring.Emilio Jesus Gallego Arias
2020-03-19[declare] Remove one use of inline_private_constantsEmilio Jesus Gallego Arias
We instead favor the `build_by_tactic` function which should at some point better integrated in the declare core.
2020-03-19[declare] More uniformity in arguments labels / namesEmilio Jesus Gallego Arias
In anticipation for more consolidation of duplicated functionality.
2020-03-19[declare] Bring more consistency to parameters using labelsEmilio Jesus Gallego Arias
Most of the parameters were named, we fix the remaining cases.
2020-03-19Merge PR #11862: Fix deprecation warning in sphinx and remove workaround for ↵Théo Zimmermann
fixed bug Reviewed-by: Zimmi48
2020-03-19Merge PR #11745: Remove invisible U+FE00 variation selector from CoqIDE bindingsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-19[refman] Stop using the deprecated math_block node (fixed GH-11856)Clément Pit-Claudel
2020-03-19[refman] Remove workaround for sphinx-doc/sphinx#4983Clément Pit-Claudel
2020-03-19Interpret the Export modifier of Set and Unset as an attribute.Théo Zimmermann
Unfortunately, we cannot go further and parse Export as a legacy attribute because this syntax conflicts with the Export command.
2020-03-19Update fullGrammar, common.edit_mlg and orderedGrammar...Théo Zimmermann
following changes to attribute parsing.
2020-03-19Document all the existing attributes.Théo Zimmermann
And fix documentation following the removal of the Template Check flag in #11546.
2020-03-19Make Cumulative, NonCumulative and Private attributes.Théo Zimmermann
- Legacy attributes can now be specified in any order. - Legacy attribute Cumulative maps to universes(cumulative). - Legacy attribute NonCumulative maps to universes(noncumulative). - Legacy attribute Private maps to private(matching). We use "private(matching)" and not "private(match)" because we cannot use keywords within attributes.
2020-03-19Update fullGrammar and common.edit_mlg following #11839.Théo Zimmermann
2020-03-19Merge PR #11760: firstorder: default tactic is “auto with core”Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:57:56 +0000