aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
We remove most of what was deprecated in `Term`. Now, `intf` and `kernel` are almost deprecation-free, tho I am not very convinced about the whole `Term -> Constr` renaming but I'm afraid there is no way back. Inconsistencies with the constructor policy (see #6440) remain along the code-base and I'm afraid I don't see a plan to reconcile them. The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a good idea as someone added a `List` module inside it.
2018-05-30[api] Remove deprecated aliases from `Names`.Emilio Jesus Gallego Arias
2018-05-30[api] Reintroduce `Names.global_reference` aliasEmilio Jesus Gallego Arias
Due to a bad interaction between PRs, the `Names.global_reference` alias was removed in 8.9, where it should disappear in 8.10. The original PR #6156 deprecated the alias in `Libnames`.
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-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[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-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
2018-05-25Merge PR #7598: Fix recipe for FAKEIDEBYTEEnrico Tassi
2018-05-24[tactics] Remove anonymous fix/cofix form.Emilio Jesus Gallego Arias
We remove the `fix N / cofix N` forms from the tactic language. This way, these tactics don't depend anymore on the proof context, in particular on the proof name, which seems like a fragile practice. Apart from the concerns wrt maintenability of proof scripts, this also helps making the "proof state" functional; as we don't have to propagate the proof name to the tactic layer.
2018-05-24Fix recipe for FAKEIDEBYTEGaëtan Gilbert
Caused by a semantic conflict with the separate toplevels PR.
2018-05-24Merge PR #7574: Improve merging and overlay documentations.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:31:36 +0000