aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-28Tactics.introduction: remove dangerous option ~checkEnrico Tassi
In locally nameless mode (proof mode) names in the context *must* be distinct otherwise the term representation makes no sense.
2018-05-28Improve the last section of the Gallina chapter.Théo Zimmermann
2018-05-28Chapter 1 of the refman compiles without reporting any undocumented object.Théo Zimmermann
2018-05-28Improve sections on (Co)Fixpoint of the Gallina chapter.Théo Zimmermann
2018-05-28Use user printer for terms instead of debug printerMaxime Dénès
2018-05-28Add CHANGES entryMaxime Dénès
2018-05-28Fix #7333: vm_compute segfaults / Anomaly with cofixMaxime Dénès
We eta-expand cofixpoints when needed, so that their call-by-need evaluation is correctly implemented by VM and native_compute.
2018-05-28Mention test-suite in PR templateJason Gross
Close #7617
2018-05-28Unify pre_env and envMaxime Dénès
We now have only two notions of environments in the kernel: env and safe_env.
2018-05-28Remove vm_conv hook and reorganize kernel filesMaxime Dénès
2018-05-28Make some comments more precise about compilation of cofixpointsMaxime Dénès
2018-05-28Less confusing debug printing of setfield bytecode instructionMaxime Dénès
2018-05-28Merge PR #7419: Remove 100 occurrences of Evd.emptyPierre-Marie Pédrot
2018-05-27Improve subsection on co-inductive types of the Gallina chapter.Théo Zimmermann
2018-05-27Simplify the code that handles trust of side-effects in kernel typing.Pierre-Marie Pédrot
For some reason the code was returning int option when only the value of the integer was relevant.
2018-05-27Adapt to coq/coq#7558.Emilio Jesus Gallego Arias
Trivial renaming of the vernacular parsing entry point.
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias
We make the vernacular implementation self-contained in the `vernac/` directory. To this extent we relocate the parser, printer, and AST to the `vernac/` directory, and move a couple of hint-related types to `Hints`, where they do indeed belong. IMO this makes the code easier to understand, and provides a better modularity of the codebase as now all things under `tactics` have 0 knowledge about vernaculars. The vernacular extension machinery has also been moved to `vernac/`, this will help when #6171 [proof state cleanup] is completed along with a stronger typing for vernacular interpretation that can distinguish different types of effects vernacular commands can perform. This PR introduces some very minor source-level incompatibilities due to a different module layering [thus deprecating is not possible]. Impact should be relatively minor.
2018-05-27[tactics] Turn boolean locality hint parameter into a named one.Emilio Jesus Gallego Arias
2018-05-27[api] [parsing] Move Egram* to `vernac/`Emilio Jesus Gallego Arias
The extension mechanism is specific to metasyntax and vernacinterp, thus it makes sense to place them next to each other. We also fix the META entry for the `grammar` camlp5 plugin.
2018-05-27Improve subsection on mutual inductive types of the Gallina chapter.Théo Zimmermann
2018-05-27Move 'new in Coq 8.1' subsection to an appropriate place.Théo Zimmermann
2018-05-27Document Variant properly.Théo Zimmermann
Cf. Enrico's remark at https://github.com/coq/coq/pull/7536#issuecomment-389826121 This commit also marginally improves the Record doc (a lot more remains to do).
2018-05-27Improve inductive types subsection of the Gallina chapter.Théo Zimmermann
2018-05-27Merge PR #7573: Remove unused Printer.printer_pr override mechanism.Hugo Herbelin
2018-05-26Merge PR #7543: [ide] Move common protocol library to its own folder/object.Pierre-Marie Pédrot
2018-05-26Improve subsection Definitions of the Gallina chapter.Théo Zimmermann
2018-05-26Improve subsection Assumptions of the Gallina chapter.Théo Zimmermann
2018-05-26Merge PR #7603: Use -j 1 for high memory fiat crypto targetsEmilio Jesus Gallego Arias
2018-05-26Merge PR #7285: Give advice on managing GitHub notifications in CONTRIBUTING.Maxime Dénès
2018-05-26Improve the section Terms of the Gallina chapter.Théo Zimmermann
Including adding missing irrefutable-patterns to the grammar of binders.
2018-05-26Merge PR #6057: Start a release process documentation.Maxime Dénès
2018-05-25Allow make clean to work on a fresh cloneJason Gross
The file `config/Makefile` doesn't exist unless we run `./configure`. We shouldn't have to run `./configure` to run `make clean`. We now no longer error in any case if `config/Makefile` doesn't exist; this is simpler than only not erroring if the target is `clean`. We also now test this property when building on CI. This fixes #7542
2018-05-25[doc] Allow more than one signature and name per Sphinx objectClément Pit-Claudel
As discussed in GH-7556.
2018-05-25Merge pull request #7569 from ppedrot/clean-newringAssia Mahboubi
Simplify the newring hack
2018-05-25Renaming global_reference according to Coq PR #6156.Hugo Herbelin
2018-05-25Renaming smartmap and fold_map according to Coq PR #7177.Hugo Herbelin
2018-05-25Merge PR #7524: [ssr] fix after to_constr ~abort_on_undefined_evars was addedMaxime Dénès
2018-05-25Merge PR #7467: Remove unused references from biblio.Maxime Dénès
2018-05-25Merge PR #7551: Update CODEOWNERS (mostly regarding the test-suite)Maxime Dénès
2018-05-25Change primary maintainer for the checker.Théo Zimmermann
Primary maintainers should be responsive. [ci skip]
2018-05-25Fix notation for code snippet in documentationAnton Trunov
It failed to compile before because the type arguments were declared implicit after introducing the notation
2018-05-25Merge PR #7556: Add a setting to warn about empty object in the refmanMaxime Dénès
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
We address the easy ones, but they should probably be all removed.
2018-05-25An attempt to clarify error message for Arguments needing "rename" flag.Hugo Herbelin
Using a formulation which makes it is clear that no renaming has been done. See discussion at issue #2987.
2018-05-25Use -j 1 for high memory fiat crypto targetsGaëtan Gilbert
2018-05-25Merge PR #7508: Improve rewrite section in tactic chapter.Maxime Dénès
2018-05-25Merge PR #7533: [sphinx] Bump timeout. Closes #7532.Maxime Dénès
2018-05-25Merge pull request coq/ltac2#58 from ejgallego/tactics+push_fix_naming_outPierre-Marie Pédrot
Adapt to fix/cofix changes in Coq (coq/coq#7196)
2018-05-25Merge PR #7196: [tactics] Remove anonymous fix/cofix form.Pierre-Marie Pédrot
2018-05-25Merge PR #7325: Fix #7323: coqchk puts polymorphic univs of inductive in ↵Pierre-Marie Pédrot
global env
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 16:49:05 +0000