aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-31Indicate in the doc that clearbody can take several identsThéo Winterhalter
2018-05-31Merge PR #7578: Allow make clean to work on a fresh cloneEnrico Tassi
2018-05-31Merge PR #7639: Makefile: fix undefined NATIVEFILES when -native-compute noEnrico Tassi
2018-05-31Merge PR #7633: [Makefile] New target “install-merlin”Enrico Tassi
2018-05-30Merge PR #7260: Fix #6951: Unexpected error during scheme creation.Maxime Dénès
2018-05-30Merge PR #7558: [api] Make `vernac/` self-contained.Maxime Dénès
2018-05-30Merge PR #7621: Tactics.introduction: remove dangerous option ~checkPierre-Marie Pédrot
2018-05-30Makefile: fix undefined NATIVEFILES when -native-compute noGaëtan Gilbert
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-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-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-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-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-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-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-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-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-25Merge pull request #7569 from ppedrot/clean-newringAssia Mahboubi
Simplify the newring hack
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-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-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 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-04-27 14:17:55 +0000