aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-02Add Equations overlayMatthieu Sozeau
2018-07-02Merge PR #7969: doc: typesetting and hyperlinks in Syntax ExtensionsThéo Zimmermann
2018-07-02Merge PR #7965: doc: Fix typesetting in Gallina extensionsThéo Zimmermann
2018-07-02Clean up documentation around beginner's guide.Siddharth Bhat
- move `README` to `README.md` to take advantage of markdown features - remove `setup.txt`, port the editor specific information to the wiki. Merge development information into `dev/doc/README.md`. Wiki merge link: https://github.com/coq/coq/wiki/DevelSetup. - Add new links to files into `dev/README.md`. - Remove stale `translate.txt`.
2018-07-02[envars] honor env variable COQLIBEnrico Tassi
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables
2018-07-02Merge pull request coq/ltac2#65 from ppedrot/camlp5-parserPierre-Marie Pédrot
Fix for compilation with the camlp5-parser branch.
2018-07-02Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵Emilio Jesus Gallego Arias
points of Camlp5
2018-07-02Merge PR #7961: [api] Fix wrong deprecation warning (#7915)Enrico Tassi
2018-07-02Adding back ocp-index to default.nix.Théo Zimmermann
2018-07-02Fix default.nix following a package renaming.Théo Zimmermann
2018-07-01Document option Uniform Inductive ParametersJasper Hugunin
2018-07-01Add test for Uniform Inductive ParametersJasper Hugunin
2018-07-01Add flag Uniform Inductive ParametersJasper Hugunin
2018-07-01Implement uniform parameters in ComInductiveJasper Hugunin
Don't allow notations attached to uniform inductives
2018-07-01[api] Fix wrong deprecation warning (#7915)Emilio Jesus Gallego Arias
Fixes: #7915. Due to a change in the original misctypes removal PR, the deprecation notice went out of sync.
2018-07-01Merge PR #7964: Document that GITURL variables shouldn't have a trailing ↵Emilio Jesus Gallego Arias
.git anymore.
2018-07-01Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵Emilio Jesus Gallego Arias
Z into three files
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-29More efficient abstraction over variables in Cooking.Pierre-Marie Pédrot
Instead of repeatedly replacing the variables with a De Bruijn index and closing it, we do this in one pass. We furthermore share the abstraction over the context. This source of slowdown was observed in lambda-rust.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 11:07:10 +0000