aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2020-03-18[ci] [docker] Update to 4.09.1Emilio Jesus Gallego Arias
That release includes non trivial changes related C compilers, in particular due to `-fno-common` support.
2020-03-18Merge PR #11607: Hide binder type in Ltac2Jason Gross
Reviewed-by: JasonGross Ack-by: SkySkimmer
2020-03-18Adding a round-trip test for binders.Pierre-Marie Pédrot
2020-03-18Actually use the binder type for Ltac2 that should be used in the kernel.Pierre-Marie Pédrot
That is, it contains the type of the binder so as not to rely on the relevance explicitly.
2020-03-18Hide the Ltac2 binder type.Pierre-Marie Pédrot
For robustness and it is better to leave it opaque. Users are not supposed to fiddle with it.
2020-03-18Rename Retypeops -> RelevanceopsGaëtan Gilbert
This module used to do retyping for the kernel in prototypes of SProp, but was switched to only relevance inference before the merge.
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
Reviewed-by: jfehrle
2020-03-18Merge PR #11812: Add an Export locality to hintsThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: gares Ack-by: maximedenes
2020-03-18Merge PR #11839: Dead code in g_prim.mlgPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-18Adding overlays.Pierre-Marie Pédrot
2020-03-18Add documentation for the export hint.Pierre-Marie Pédrot
2020-03-18Export the user-facing attribute for hint locality.Pierre-Marie Pédrot
2020-03-18Also show unchanged headers.Théo Zimmermann
2020-03-18Remove dates in headers.Théo Zimmermann
Cf. discussion at #11559 and decision of Coq Call 2020-02-26.
2020-03-18Use a 3-valued flag for hint locality.Pierre-Marie Pédrot
We reuse the same type as for options, even though it is a bit ill-named. At least it allows to share code with it.
2020-03-18Hack a non-superglobal mode for hints.Pierre-Marie Pédrot
The current implementation was seemingly never thought for this kind of semantics. Everything is superglobal by construction, notably hint database creation and naming schemes. The new mode feels a bit hackish to me, at some point this should be fully reimplemented from scratch with a clear design in mind.
2020-03-18Change some ouput tests due to the printing of implicitsSimonBoulier
2020-03-18Merge PR #11746: Register commonly used names from the Reals library for ↵Théo Zimmermann
plugins (e.g. gappa) Reviewed-by: Zimmi48
2020-03-17Properly thread let-bindings in Funind principle construction.Pierre-Marie Pédrot
Fixes #11846: Funind fails to generate principles for terms with let bindings.
2020-03-17Merge PR #11699: Comment difference between the 2 hashes on constrPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-17Merge PR #11825: [ci] [docker] Update components in Docker imageGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-17Merge PR #11811: Remove a positivity check when Positivity Checking is offGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-17Add test for PR11811 (disable a positivity check)SimonBoulier
2020-03-17Dead code in g_prim.mlgHugo Herbelin
2020-03-16[ci] Cleanup old overlays.Emilio Jesus Gallego Arias
2020-03-16[ci] [docker] Update components in Docker imageEmilio Jesus Gallego Arias
We bump ounit, odoc, and lablgtk3 ; so far this is routine maintenance.
2020-03-16Merge PR #11813: Fixed link to "match" syntax figures.Théo Zimmermann
Reviewed-by: Zimmi48
2020-03-16Merge PR #11831: [ci] Re-enable VST testingGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-16Document coq_makefile behavior wrt -native-compiler yesPierre Roux
2020-03-16Fix coq-makefile/native1 testPierre Roux
This was accidentaly disabled by #6264 when no_native_compiler was renamed to native_compiler. Moreover, the (then unactivated test) was broken by commit 48ae6ce (part of #9088).
2020-03-15[ci] Re-enable VST testingEmilio Jesus Gallego Arias
VST has been fixed upstream, c.f. https://github.com/PrincetonUniversity/VST/issues/392
2020-03-15Use quotes when "necessary" in the coqtop argument window.Hugo Herbelin
This is at least to be able to use spaces in file names (#11595). In practice it protects also \, ', ", and many other symbols.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-18 07:00:27 +0000