aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-03-20python3 script does not need to import from the futureRalf Treinen
2020-03-20Add an index for attributes.Théo Zimmermann
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
2020-03-19Adapt to sub-TOC not showing in PDF output.Théo Zimmermann
2020-03-19[refman] Move chapters into new structure.Théo Zimmermann
As a first step toward a deeper refactoring of the reference manual, we move existing chapters into a new structure. We use the Sphinx support for top-level chapters spanning multiple pages to consolidate existing chapters into a smaller number of chapters and a smaller number of parts. Now the full top-level table of content can be seen in one glance. Most of the new chapters are divided into several sub-chapters (on separate pages) that correspond to the pre-existing chapters. These new top-level chapters gathering several chapters together have gained a new introduction. The main introduction has been rewritten / simplified as well. For now, the URL of pre-existing chapters does not change. The intent is to further refactor the manual by splitting some of these sub-chapters into smaller ones, and by moving things around. While the sub-chapters are likely to evolve very much in the future, the top-level table of content is almost final (except that the "Using Coq" part may gain one or two additional chapters on proof engineering / project management). Thanks to Jim Fehrle for investigating how to split a chapter on multiple pages and to both Jim and Matthieu Sozeau for the discussion that led to this new structure. See also the related CEP: https://github.com/coq/ceps/pull/43 Additional notes: - A new directory structure has been created reflecting the new chapter structure. - The indexes chapter has been removed from the PDF version since it wasn't working. Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-03-19Remove spurious anomalies in kernel reductionGaëtan Gilbert
2020-03-19Merge PR #11860: [ci] [docker] Update to 4.09.1Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-19Fuck off ocamlformat.Pierre-Marie Pédrot
2020-03-19Reduce the scope of a call to pervasive equality in Coq_micromega.Pierre-Marie Pédrot
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
Ack-by: herbelin
2020-03-19Merge PR #11822: Grants #11692: clear dependent knows about let-inPierre-Marie Pédrot
Reviewed-by: JasonGross Reviewed-by: ppedrot
2020-03-19Use monomorphic comparison functions in Micromega.Vect.Pierre-Marie Pédrot
2020-03-19Dedicate type for monomials in Micromega.Vect.Pierre-Marie Pédrot
This enforces monomorphism everywhere possible.
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-19[stdlib] Remove a few `auto with *`Vincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 01:21:58 +0000