Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | | * | | [ci] [docker] Make sure we don't install optional packages with apt. | Emilio Jesus Gallego Arias | 2018-07-02 | |
* | | | | | | | | Merge PR #7703: Add an option to force parameters to be uniform | Matthieu Sozeau | 2018-07-02 | |
|\ \ \ \ \ \ \ \ | ||||
| | | | | | | | * | Rename the "chan" argument into "fmt" in coqpp_main. | Pierre-Marie Pédrot | 2018-07-02 | |
| | | | | | | | * | Remove the hardcoded compatibility wit_hyp -> wit_var from the parser. | Pierre-Marie Pédrot | 2018-07-02 | |
| | | | | | | | * | Slight simplification of the Tacentries API to register ML tactics. | Pierre-Marie Pédrot | 2018-07-02 | |
| | | | | | | | * | Documenting the syntax changes. | Pierre-Marie Pédrot | 2018-07-02 | |
| | | | | | | | * | Moving various ml4 files to mlg. | Pierre-Marie Pédrot | 2018-07-02 | |
| | | | | | | | * | Implementing TACTIC EXTEND in coqpp. | Pierre-Marie Pédrot | 2018-07-02 | |
| | | | | | | |/ | ||||
| | | | | * | | | Add Equations overlay | Matthieu Sozeau | 2018-07-02 | |
* | | | | | | | | Merge PR #7969: doc: typesetting and hyperlinks in Syntax Extensions | Théo Zimmermann | 2018-07-02 | |
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #7965: doc: Fix typesetting in Gallina extensions | Théo Zimmermann | 2018-07-02 | |
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ |/| | | | | | | | | ||||
| | | | | | * | | | Clean up documentation around beginner's guide. | Siddharth Bhat | 2018-07-02 | |
| |_|_|_|_|/ / / |/| | | | | | | | ||||
| | | | * | | | | [envars] honor env variable COQLIB | Enrico Tassi | 2018-07-02 | |
| | | | | | * | | hints: add Hint Variables/Constants Opaque/Transparent commands | Matthieu Sozeau | 2018-07-02 | |
| |_|_|_|_|/ / |/| | | | | | | ||||
* | | | | | | | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points... | Emilio Jesus Gallego Arias | 2018-07-02 | |
|\ \ \ \ \ \ \ | |_|_|_|/ / / |/| | | | | | | ||||
* | | | | | | | Merge PR #7961: [api] Fix wrong deprecation warning (#7915) | Enrico Tassi | 2018-07-02 | |
|\ \ \ \ \ \ \ | ||||
| | | | | | * | | Adding back ocp-index to default.nix. | Théo Zimmermann | 2018-07-02 | |
| | | | | | * | | Fix default.nix following a package renaming. | Théo Zimmermann | 2018-07-02 | |
| |_|_|_|_|/ / |/| | | | | | | ||||
| | | | | * | | Document option Uniform Inductive Parameters | Jasper Hugunin | 2018-07-01 | |
| | | | | * | | Add test for Uniform Inductive Parameters | Jasper Hugunin | 2018-07-01 | |
| | | | | * | | Add flag Uniform Inductive Parameters | Jasper Hugunin | 2018-07-01 | |
| | | | | * | | Implement uniform parameters in ComInductive | Jasper Hugunin | 2018-07-01 | |
| |_|_|_|/ / |/| | | | | | ||||
| * | | | | | [api] Fix wrong deprecation warning (#7915) | Emilio Jesus Gallego Arias | 2018-07-01 | |
|/ / / / / | ||||
* | | | | | Merge PR #7964: Document that GITURL variables shouldn't have a trailing .git... | Emilio Jesus Gallego Arias | 2018-07-01 | |
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, Z... | Emilio Jesus Gallego Arias | 2018-07-01 | |
|\ \ \ \ \ \ | ||||
* \ \ \ \ \ \ | Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f... | Emilio Jesus Gallego Arias | 2018-07-01 | |
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR #7759: Workaround to fix #7731 (printing not splitting line at break... | Emilio Jesus Gallego Arias | 2018-07-01 | |
|\ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | doc: typesetting and hyperlinks in Syntax Extensions | Lysxia | 2018-06-30 | |
* | | | | | | | | | Merge PR #7960: [build] Remove target binary before copy. | Enrico Tassi | 2018-06-30 | |
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR #7949: Split the Ssrmatching module between code and grammar rules. | Enrico Tassi | 2018-06-30 | |
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / |/| | | | | | | | | | ||||
| * | | | | | | | | | Split the Ssrmatching module between code and grammar rules. | Pierre-Marie Pédrot | 2018-06-30 | |
|/ / / / / / / / / | ||||
| | | | | | * | | | Adding an overlay for the PR. | Pierre-Marie Pédrot | 2018-06-29 | |
| | | | | | * | | | Documenting the transition strategy of GEXTEND. | Pierre-Marie Pédrot | 2018-06-29 | |
| | | | | | * | | | Port g_tactic to the homebrew GEXTEND parser. | Pierre-Marie Pédrot | 2018-06-29 | |
| | | | | | * | | | Port g_toplevel to the homebrew GEXTEND parser. | Pierre-Marie Pédrot | 2018-06-29 | |
| | | | | | * | | | Port g_vernac to the homebrew GEXTEND parser. | Pierre-Marie Pédrot | 2018-06-29 | |
| | | | | | * | | | Port g_proofs to the homebrew GEXTEND parser. | Pierre-Marie Pédrot | 2018-06-29 | |
| | | | | | * | | | Port g_constr to the homebrew GEXTEND parser. | Pierre-Marie Pédrot | 2018-06-29 | |
| | | | | | * | | | Port g_prim to the homebrew GEXTEND parser. | Pierre-Marie Pédrot | 2018-06-29 | |
| | | | | | * | | | Use a homebrew parser to replace the GEXTEND extension points of Camlp5. | Pierre-Marie Pédrot | 2018-06-29 | |
| |_|_|_|_|/ / / |/| | | | | | | | ||||
| | | | | | * | | doc: Fix typesetting in Gallina extensions | Lysxia | 2018-06-29 | |
| |_|_|_|_|/ / |/| | | | | | | ||||
| | | | | * | | Document that GITURL variables shouldn't have a trailing .git anymore. | Théo Zimmermann | 2018-06-29 | |
| |_|_|_|/ / |/| | | | | | ||||
* | | | | | | Merge PR #7918: Mini-update of version history with recent changes. | Théo Zimmermann | 2018-06-29 | |
|\ \ \ \ \ \ | ||||
| | | | | * | | Splitting primitive numeral parser/printer for positive, N, Z into three files. | Hugo Herbelin | 2018-06-29 | |
| | | * | | | | Workaround to fix #7731 (printing not splitting line at break hint). | Hugo Herbelin | 2018-06-29 | |
| | | | |/ / | | | |/| | | ||||
| | | | * | | Fixes #7712 (an anomaly in reporting bad recursive notation format). | Hugo Herbelin | 2018-06-29 | |
| | | |/ / | ||||
* | | | | | Merge PR #7080: Swapping Context and Constr and defining declarations on cons... | Maxime Dénès | 2018-06-29 | |
|\ \ \ \ \ | ||||
| | | * | | | [build] Remove target binary before copy. | Emilio Jesus Gallego Arias | 2018-06-29 | |
| |_|/ / / |/| | | | | ||||
* | | | | | Merge PR #7890: Inline a function from Quote used in setoid_ring. | Maxime Dénès | 2018-06-29 | |
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR #7745: Make type Environ.globals abstract + simplify Environ.retrokn... | Maxime Dénès | 2018-06-29 | |
|\ \ \ \ \ \ |