aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-07-03fix syntax of .mlgVincent Laporte
2018-07-03Describe attributes in the documentation.Vincent Laporte
2018-07-03[vernac] use a record for the contents of the “deprecated” attributeVincent Laporte
2018-07-03[vernac] use plain strings as attribute namesVincent Laporte
2018-07-03[vernac] indentationVincent Laporte
2018-07-03[vernac] Generic syntax for flags/attributesVincent Laporte
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
2018-07-03Merge PR #7978: [ci] [docker] Make sure we don't install optional packages wi...Gaëtan Gilbert
2018-07-03Merge PR #7607: Simplify reification of predicate in bytecode and native comp...Pierre-Marie Pédrot
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 ./conf...Emilio Jesus Gallego Arias
2018-07-02[ci] [docker] Make sure we don't install optional packages with apt.Emilio Jesus Gallego Arias
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
2018-07-02[envars] honor env variable COQLIBEnrico Tassi
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-07-02Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points...Emilio Jesus Gallego Arias
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
2018-07-01[api] Fix wrong deprecation warning (#7915)Emilio Jesus Gallego Arias
2018-07-01Merge PR #7964: Document that GITURL variables shouldn't have a trailing .git...Emilio Jesus Gallego Arias
2018-07-01Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, Z...Emilio Jesus Gallego Arias
2018-07-01Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...Emilio Jesus Gallego Arias
2018-07-01Merge PR #7759: Workaround to fix #7731 (printing not splitting line at break...Emilio Jesus Gallego Arias
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
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