aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-01Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation ↵Emilio Jesus Gallego Arias
format).
2018-07-01Merge PR #7759: Workaround to fix #7731 (printing not splitting line at ↵Emilio Jesus Gallego Arias
break hint).
2018-06-30Suppress useless "true bin/*.opt.exe" messages from no-op STRIP and CODESIGN ↵Jim Fehrle
steps.
2018-06-30Rebuild coqtop$(EXE) in "make coqbinaries" in addition to coqtop.opt$(EXE).Jim Fehrle
Fixes #7758.
2018-06-30doc: typesetting and hyperlinks in Syntax ExtensionsLysxia
2018-06-30Merge PR #7960: [build] Remove target binary before copy.Enrico Tassi
2018-06-30Merge PR #7949: Split the Ssrmatching module between code and grammar rules.Enrico Tassi
2018-06-30Split the Ssrmatching module between code and grammar rules.Pierre-Marie Pédrot
Fixes #7857.
2018-06-29Adding an overlay for the PR.Pierre-Marie Pédrot
2018-06-29Documenting the transition strategy of GEXTEND.Pierre-Marie Pédrot
2018-06-29Port g_tactic to the homebrew GEXTEND parser.Pierre-Marie Pédrot
2018-06-29Port g_toplevel to the homebrew GEXTEND parser.Pierre-Marie Pédrot
2018-06-29Port g_vernac to the homebrew GEXTEND parser.Pierre-Marie Pédrot
2018-06-29Port g_proofs to the homebrew GEXTEND parser.Pierre-Marie Pédrot
2018-06-29Port g_constr to the homebrew GEXTEND parser.Pierre-Marie Pédrot
2018-06-29Port g_prim to the homebrew GEXTEND parser.Pierre-Marie Pédrot
2018-06-29Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Pierre-Marie Pédrot
The parser is stupid and the syntax is almost the same as the previous one. The only difference is that one needs to wrap OCaml code between { braces } so that quoting works out of the box. Files requiring such a syntax are handled specifically by the type system and need to have a .mlg extension instead of a .ml4 one.
2018-06-29doc: Fix typesetting in Gallina extensionsLysxia
2018-06-29Document that GITURL variables shouldn't have a trailing .git anymore.Théo Zimmermann
This allows to append /archive at the end.
2018-06-29Merge PR #7918: Mini-update of version history with recent changes.Théo Zimmermann
2018-06-29Splitting primitive numeral parser/printer for positive, N, Z into three files.Hugo Herbelin
2018-06-29Workaround to fix #7731 (printing not splitting line at break hint).Hugo Herbelin
In some cases, Format's inner boxes inside an outer box act as break hints, even though there are already "better" break hints in the outer box. We work around this "feature" by not inserting a box around the default printing rule for a notation if there is no effective break points in the box. See https://caml.inria.fr/mantis/view.php?id=7804 for the related OCaml discussion.
2018-06-29Fixes #7712 (an anomaly in reporting bad recursive notation format).Hugo Herbelin
2018-06-29Merge PR #7080: Swapping Context and Constr and defining declarations on ↵Maxime Dénès
constr in Constr
2018-06-29[build] Remove target binary before copy.Emilio Jesus Gallego Arias
Fixes #7666. Due to shared mapping of executables Linux doesn't allow to overwrite binaries that are running; we do as `ocamlopt` and delete the target file before copy.
2018-06-29Merge PR #7890: Inline a function from Quote used in setoid_ring.Maxime Dénès
2018-06-29Merge PR #7745: Make type Environ.globals abstract + simplify ↵Maxime Dénès
Environ.retroknowledge
2018-06-29Merge PR #7950: Documentation for 8.8.1Maxime Dénès
2018-06-28Merge PR #7860: Fix #7704: Launching coqide through PATH fails.Emilio Jesus Gallego Arias
2018-06-28CHANGES for 8.8.1.Théo Zimmermann
2018-06-28Self-credit for the work done.Théo Zimmermann
I reused the sentence from the version 8.7 credits. It wasn't initially decided like this but it looks like I'm the de facto maintainer for this release as well.
2018-06-28Merge PR #7948: Syntax for naming an existential variableThéo Zimmermann
2018-06-28Merge PR #7928: Fix 'unbound variable' issue on Windows packaging jobs.Michael Soegtrop
2018-06-28wrong sphinx syntaxAmbroise
2018-06-28Merge PR #7946: Update maintainers for native/VM files in pretypingThéo Zimmermann
2018-06-28Update gallina-extensions.rstAmbroise
I knew this feature existed but I did not remember the syntax and I could not find it in the manual
2018-06-28Merge PR #7937: Mention Consortium in READMEThéo Zimmermann
2018-06-28Merge PR #7917: Critical bugs: added #3243 and Gonthier's bug in lazy machine.Théo Zimmermann
2018-06-28Deprecate Environ.retroknowledge function in favor of the projectionGaëtan Gilbert
2018-06-28[env.env_rel_context.env_rel_ctx] -> [rel_context env]Gaëtan Gilbert
It's a bit shorter and more direct.
2018-06-28Make Environ.globals abstract.Gaëtan Gilbert
2018-06-28Simplify reification of predicate in bytecode and native compilersMaxime Dénès
I believe this is legacy code due to a previous, more complex representation of return predicates in the kernel.
2018-06-28Merge PR #7932: CoqIDE scrolls the proof buffer down to the first goal.Pierre-Marie Pédrot
2018-06-28Update maintainers for native/VM files in pretypingMaxime Dénès
2018-06-28Merge PR #7866: Implementation of mutual records in the higher strataMaxime Dénès
2018-06-28Merge PR #7934: Add mit-plv/bedrock2-ci to CIEmilio Jesus Gallego Arias
2018-06-27Add mit-plv/bedrock2-ci to CIAndres Erbsen
2018-06-27Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Pierre-Marie Pédrot
2018-06-27Merge PR #7939: Turn the CoqProject_file module into a pure ML fileEmilio Jesus Gallego Arias
2018-06-27Mention Consortium in READMEMaxime Dénès
We are now actively looking for sponsors, let's make our communication more visible.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 15:00:31 +0000