aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-30Merge pull request #6 from maximedenes/fix-printerYves Bertot
Use user printer for terms instead of debug printer
2018-05-30Fix an outdated comment refering to lib/dnet.mliArmaël Guéneau
2018-05-29Merge PR #7593: Don't try to install native compiled files if native-compile ↵Maxime Dénès
is not set
2018-05-29Fix #6951: Unexpected error during scheme creation.Pierre-Marie Pédrot
When creating a scheme for bifinite inductive types, we do not create a fixpoint.
2018-05-29Merge PR #7566: Remove a dead old-refman file.Maxime Dénès
2018-05-29Merge PR #7628: [default.nix] Update dependency listThéo Zimmermann
2018-05-29Merge PR #7626: Test for #7333 (soundness with VM/native and cofix)Théo Zimmermann
2018-05-29[Makefile] New target “install-merlin”Vincent Laporte
Building this target installs the files that are used by merlin: - .merlin files (.merlin); - bin-annot files (.cmt, .cmti); - source files (.ml, .mli). Plug-in developpers can thus work with an “installed” version of Coq.
2018-05-29Fix anomaly in autoapply when an unbound hint name is providedArmaël Guéneau
2018-05-29[default.nix] Adds “ounit” to check dependenciesVincent Laporte
2018-05-29[default.nix] List “hostname” as a dependencyVincent Laporte
2018-05-29[default.nix] Use OCaml 4.06Vincent Laporte
2018-05-29[default.nix] Drop dependency to ocp-indexVincent Laporte
2018-05-29Merge PR #7084: [default.nix] Unpin nixpkgsThéo Zimmermann
2018-05-29Add test for #7333: vm_compute segfaults / Anomaly with cofixMaxime Dénès
2018-05-28Merge PR #7521: Fix soundness bug with VM/native and cofixpointsPierre-Marie Pédrot
2018-05-28Fix w.r.t. coq/coq#7521.Pierre-Marie Pédrot
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 04:03:22 +0000