aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-03[vernac] Generic parsing rules for attributesVincent Laporte
2018-07-03[vernac] Add a “deprecated” attributeVincent Laporte
2018-07-03Allow “Let”-defined coercionsVincent Laporte
2018-07-03[vernac] Concrete syntax for attributesVincent Laporte
2018-07-03[vernac] mk_atts: an atts record with default valuesVincent Laporte
2018-07-03[vernac] attribute_of_flagsVincent Laporte
Elaborate a [atts] record out of a list of flags.
2018-07-03Merge PR #7978: [ci] [docker] Make sure we don't install optional packages ↵Gaëtan Gilbert
with apt.
2018-07-03Merge PR #7607: Simplify reification of predicate in bytecode and native ↵Pierre-Marie Pédrot
compilers
2018-07-03Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsPierre-Marie Pédrot
2018-07-03Merge PR #7942: Extend readme with 'beginners guide'Théo Zimmermann
2018-07-03Merge PR #7974: Fix default.nix following a package renaming.Vincent Laporte
2018-07-03Merge PR #7977: allow `make check` to succeed when -prefix is given to ↵Emilio Jesus Gallego Arias
./configure and make install not run yet
2018-07-02[ci] [docker] Make sure we don't install optional packages with apt.Emilio Jesus Gallego Arias
This should help towards ensuring that the system only has the packages we specify in the Dockerfile. We were missing: - `git`: used in the CI system itself! - `rsync`: used in the test-suite - `python3-setuptools`, `python3-wheel`: necessary to use pip3 properly to install the missing python package. - `autoconf`, `automake`: a few CI contribs depend on them.
2018-07-02Merge PR #7703: Add an option to force parameters to be uniformMatthieu Sozeau
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 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:35:58 +0000