aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-29Merge PR #7084: [default.nix] Unpin nixpkgsThéo Zimmermann
2018-05-28Merge PR #7521: Fix soundness bug with VM/native and cofixpointsPierre-Marie Pédrot
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-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
2018-05-24Remove the unused printer_pr mechanism.Jim Fehrle
2018-05-24Complete rewrite of the documentation of overlays after Jim's additional ↵Théo Zimmermann
comments. [ci skip]
2018-05-24Relax advice on the name of user-overlays following Gaëtan's suggestion.Théo Zimmermann
[ci skip]
2018-05-24Improve merging and overlay documentations.Théo Zimmermann
Clarification prompted by Jim Fehrle. [ci skip]
2018-05-24Merge PR #7177: Unifying names of "smart" combinators + adding combinators ↵Pierre-Marie Pédrot
in CArray
2018-05-24Merge PR #7594: Fix #5983 (many frequent AppVeyor failures) by increasing ↵Emilio Jesus Gallego Arias
spawn timeout.
2018-05-24Fix #7323: coqchk puts polymorphic univs of inductive in global envGaëtan Gilbert
2018-05-24[ide] Move common protocol library to its own folder/object.Emilio Jesus Gallego Arias
The `ide` folder contains two different binaries, the language server `coqidetop` and `coqide` itself. Even if these binaries are in the same folder, the only thing they have in common is that they link to the protocol files. In the OCaml world, having "doubly" linked files in the same project is considered a bit of an ugly practice, and some build tools such as Dune disallow it.q Thus, to clean up the build, we move the common protocol files to its own library `ideprotocol`. This helps towards Dune integration and towards having an IDE standalone target, such as the one that was implemented here: https://github.com/ejgallego/coqide-exp
2018-05-24Merge PR #7581: Mention warning and error message docs in PR templateThéo Zimmermann
2018-05-24Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constantsPierre-Marie Pédrot
2018-05-24Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant ↵Pierre-Marie Pédrot
instances
2018-05-24Merge PR #7575: [build] Add -cclib -lcoqrun options to build of kernel.cmxa.Enrico Tassi
2018-05-24Fix #5983 (many frequent AppVeyor failures) by increasing spawn timeout.Théo Zimmermann
2018-05-24Merge PR #7582: [ci] Build fiat-crypto targets in sequenceEmilio Jesus Gallego Arias
2018-05-24Merge PR #6515: [api] Move `Vernacexpr` to parsing.Pierre-Marie Pédrot
2018-05-23Document Smart/Array changes in dev/doc/Changes.md.Hugo Herbelin
2018-05-23Renaming miscellaneous internal smart functions.Hugo Herbelin
2018-05-23Collecting Map.smart_* functions into a module Map.Smart.Hugo Herbelin
2018-05-23Moving Rtree.smart_map into Rtree.Smart.map.Hugo Herbelin
2018-05-23Moving Option.smart_map to Option.Smart.map.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 07:39:58 +0000