aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-22Remove # keywords in PrimitivePierre Roux
2020-04-22Merge PR #11694: Support printing argument-free abbreviations in custom ↵Emilio Jesus Gallego Arias
entries with a global rule Reviewed-by: ejgallego Ack-by: gares
2020-04-21Change log for #12023Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-04-21Overlay for fiat-crypto, Mtac2, MetaCoq and UniMath.Hugo Herbelin
2020-04-21Adapt test-suite to #12023.Hugo Herbelin
2020-04-21Moving the main Require Export Ltac in Prelude.v.Hugo Herbelin
2020-04-21Adding a Declare ML Module in empty file Ltac.v.Hugo Herbelin
Indeed, it would be intuitive that `Require Import Ltac` is an equivalent for Ltac of `Require Import Ltac2.Ltac2`. Also declaring the classic proof mode.
2020-04-21Change log.Hugo Herbelin
2020-04-21Fixing #3451: coqdoc links for projections of tuples rather than for ↵Hugo Herbelin
constructor. Moreover, the link to the constructor was hiding other contents of the tuple.
2020-04-21Merge PR #12082: Fixes #11808: support for test-suite in -byte-only modeGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-21Merge PR #12149: Fix documentation following #12038.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-21Document changed warnings and erros following #12038.Théo Zimmermann
2020-04-21Constrintern: another reworking of the interning of records.Hugo Herbelin
This allows to have the "No local fields allowed in a record construction" error applicable to all fields and not only the first one. Formerly, this was wrongly raising an error "This record contains fields of both T and T".
2020-04-21Constrintern.ml: simplifying the interning of record tuples.Hugo Herbelin
We basically avoid a detour via intern_applied_reference. In particular, this stops dumpglobbing the name of the "constructor" of the record which in practice does not appear in the source.
2020-04-21Update common.edit_mlg and fullGrammar following #12038.Théo Zimmermann
2020-04-21Move documentation on Funind into a single file.Théo Zimmermann
2020-04-21Merge all documentation on Funind into the same file.Théo Zimmermann
2020-04-21Consolidate funind tactics and Functional Scheme in Funind section of the ↵Théo Zimmermann
Libraries chapter.
2020-04-21Extract funind tactics to funind section of the Libraries chapter.Théo Zimmermann
2020-04-21Remove parts of the Tactics chapter.Théo Zimmermann
2020-04-21Remove parts of the Tactics chapter.Théo Zimmermann
2020-04-21Remove everything in the Tactics chapter up-to function induction and a bit ↵Théo Zimmermann
beyond.
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
Ack-by: SkySkimmer Reviewed-by: maximedenes
2020-04-21Merge PR #12060: CoqIDE: Disable client-side decoration on WindowsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-21Merge PR #12113: Contributing guide improvementsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-21Merge PR #12137: Fix VST after PrincetonUniversity/VST#402Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-21Merge PR #12116: Fixing #12045: missing normalization in conclusion of ↵Pierre-Marie Pédrot
custom induction scheme Reviewed-by: ppedrot
2020-04-21Merge PR #12014: [stdlib] Add properties of operations on vectorsHugo Herbelin
Reviewed-by: herbelin
2020-04-21Merge PR #11883: Fix #7812: autounfold's behavior depends on file namesHugo Herbelin
Reviewed-by: herbelin
2020-04-21Fix VST after PrincetonUniversity/VST#402Gaëtan Gilbert
Specifically https://github.com/PrincetonUniversity/VST/commit/86d7ac6eaf9c580d5705c4257814f64560d24257
2020-04-21[declare] [compat] Add alias for deprecated functionEmilio Jesus Gallego Arias
2020-04-21[nit] Remove useless indirect alias.Emilio Jesus Gallego Arias
2020-04-21[declare] Remove `declare_private_constant` from the public API.Emilio Jesus Gallego Arias
This is an internal function for scheme declaration handled properly now, we can also remove `pure_definition_entry` which is IMO good too.
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias
This PR moves `Declare` to `vernac` which will hopefully allow to unify it with `DeclareDef` and avoid exposing entry internals. There are many tradeoffs to be made as interface and placement of tactics is far from clear; I've tried to reach a minimally invasive compromise: - moved leminv to `ltac_plugin`; this is unused in the core codebase and IMO for now it is the best place - hook added for abstract; this should be cleaned up later - hook added for scheme declaration; this should be cleaned up later - separation of hints vernacular and "tactic" part should be also done later, for now I've introduced a `declareUctx` module to avoid being invasive there. In particular this last point strongly suggest that for now, the best place for `Class_tactics` would be also in `ltac`, but I've avoided that for now too. This partially supersedes #10951 for now and helps with #11492 .
2020-04-21[hints] Move and split Hint Declaration AST to vernacEmilio Jesus Gallego Arias
This moves the vernacular part of hints to `vernac`; in particular, it helps removing the declaration of constants as parts of the `tactic` folder.
2020-04-20[refman] Remove references to omega from Tactics chapter.Théo Zimmermann
Omega was defined twice and this is the tactics chapter documentation which was refered to from the tactic index. We remove it so that users find the other reference (which contains the deprecation notice). The changes to the doc of zarith are a follow-up to #11976.
2020-04-20Merge PR #12038: Improve undeclared goption key messages.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-20Merge PR #12126: TIMEFMT: Display the output file nameGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-20coqdoc: Replace deprecated HTML attribute name with idLysxia
2020-04-20Merge PR #12026: Granting coqdoc wish #7093: definitions link to themselves ↵Lysxia
so as to give access to their url Reviewed-by: Lysxia
2020-04-20Adding change log for PR #12026 (definitions in coqdoc link to themselves).Hugo Herbelin
2020-04-20Granting coqdoc wish #7093 (definitions link to themselves).Hugo Herbelin
Co-Authored-By: Xia Li-yao <Lysxia@users.noreply.github.com>
2020-04-20TIMEFMT: Display the output file nameJason Gross
We now use `$@` rather than `$*` so that we display the output target rather than the stem of the rule. This is more consistent for rules that users add (where the pattern variable might be something insufficiently identifying), and also generalizes more nicely to mixing multiple compilers (we get a clear difference between producing OCaml files and producing .vo files, even if the filename is the same up to the suffix). The result is that it's easy to describe what the timing information of the build log records: each time comes with a label which is a file name, and the time is the time it takes to produce that file.
2020-04-20Remove funind tactics from Tactics chapter.Théo Zimmermann
2020-04-20Remove Functional Scheme from Scheme chapter.Théo Zimmermann
2020-04-20Move Functional Scheme to Funind section.Théo Zimmermann
2020-04-20Extract Functional Scheme from Scheme chapter.Théo Zimmermann
2020-04-20Remove coqremote stylesheets which were useless since the Sphinx migration.Théo Zimmermann
2020-04-20Remove probably useless doc/sphinx/coqdoc.css.Théo Zimmermann
2020-04-20Merge PR #12091: Adding highlighting of the target of a internal link in ↵Lysxia
default coqdoc CSS Reviewed-by: Lysxia
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 17:39:40 +0000