aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-23Merge PR #12120: Fixing #12119 : remove useless hypothesis in ↵Hugo Herbelin
NoDup_Permutation_bis Reviewed-by: herbelin
2020-04-23Merge PR #12148: Consolidate funind documentation onto a single page.Clément Pit-Claudel
Reviewed-by: jfehrle
2020-04-23Merge PR #12130: [declare] [tactics] Move declare to `vernac`Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-23[refman] Fix name of tactic: function induction -> functional induction.Théo Zimmermann
2020-04-23Fix coq snippets in Tactics chapter.Théo Zimmermann
2020-04-23Merge PR #12034: Make cumulative sprop a typing flag, deprecate command ↵Pierre-Marie Pédrot
line -sprop-cumulative Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-04-23Merge PR #12083: Tweak ltac2 grammar to make doc_grammar happyPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-22Merge PR #11928: Remove probably useless doc/sphinx/coqdoc.css.Hugo Herbelin
2020-04-22Merge PR #12031: [stdlib] A library on cyclic permutations: CPermutationHugo Herbelin
Ack-by: Zimmi48 Ack-by: anton-trunov Reviewed-by: herbelin
2020-04-22Merge PR #12133: coqdoc: Replace deprecated HTML attribute name with idHugo Herbelin
Reviewed-by: herbelin
2020-04-22Merge PR #12023: Adding a Declare ML Module in empty file Ltac.vEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: ppedrot
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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 18:40:03 +0000