| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-12-09 | [doc] Enable Warning 50 [incorrect doc comment] and fix comments. | Emilio Jesus Gallego Arias | |
| This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :) | |||
| 2018-12-05 | Remove the Like level modifier from gramlib. | Pierre-Marie Pédrot | |
| Apart from the fact we did not use it, its semantics was somewhat flaky as it was looking for any rule containing some token. | |||
| 2018-12-05 | Remove the grammar-entry correspondence dynamic check in camlp5. | Pierre-Marie Pédrot | |
| Due to the fact we only export the functorial API, this property is ensured statically. There is thus no point in checking it. | |||
| 2018-12-05 | Removing dead fields from Plexing.lexer. | Pierre-Marie Pédrot | |
| 2018-12-05 | Remove dead code in camlp5. | Pierre-Marie Pédrot | |
| The references error_verbose and strict_parsing were not accessible from the API, so their value was statically known. | |||
| 2018-12-05 | Remove the lexer field from Gramlib. | Pierre-Marie Pédrot | |
| This is useless in the functorial API. | |||
| 2018-12-05 | Make some camlp5 fields immutable. | Pierre-Marie Pédrot | |
| 2018-11-30 | [gramlib] Remove `Ploc.t` in favor of `Loc.t` | Emilio Jesus Gallego Arias | |
| The types are identical and we have no more reason for the split. Note the following TODOS: - discrepancy of `Ploc.after` with `CLexer.after` - discrepancy of `Ploc.comments` with `CLexer.comments` - `Ploc.dummy` vs `Loc.t option` | |||
| 2018-11-27 | [gramlib] Remove unused function `gram_reinit`. | Emilio Jesus Gallego Arias | |
| 2018-11-27 | [gramlib] Minor cleanups: | Emilio Jesus Gallego Arias | |
| - remove duplicate type definitions `gram_assoc`, `gram_position`, - make global `warning_verbose` variable into a parameter. | |||
| 2018-11-23 | Remove the unsafe API from gramlib. | Pierre-Marie Pédrot | |
| 2018-11-21 | [camlp5] Remove dependency on camlp5. | Emilio Jesus Gallego Arias | |
| 2018-11-19 | [gramlib] Remove unused alias. | Emilio Jesus Gallego Arias | |
| No effect on actual code. | |||
| 2018-11-06 | Removing dead code in Plexing. | Pierre-Marie Pédrot | |
| It was full with utility functions and wrappers that are unused in the Coq codebase. | |||
| 2018-11-06 | Remove the non-functorial interface of camlp5 grammars. | Pierre-Marie Pédrot | |
| 2018-11-05 | Remove patches of dead code in Gramlib. | Pierre-Marie Pédrot | |
| 2018-11-05 | Remove the Scut constructor from Gramlib. | Pierre-Marie Pédrot | |
| This constructor only makes sense in the backtracking mode, that has been removed from our vendored version of camlp5. | |||
| 2018-11-05 | Remove the Sflag constructor from Gramlib. | Pierre-Marie Pédrot | |
| It is just a wrapper around Sopt. I do not really understand why it is hardwired in the entry AST. | |||
| 2018-11-05 | Remove the Sfacto constructor from Gramlib. | Pierre-Marie Pédrot | |
| Used by rule factorisation in theory, but appears to be unused in Coq. | |||
| 2018-11-05 | Remove the Svala constructor from Gramlib. | Pierre-Marie Pédrot | |
| It is only used in strict mode, which makes no sense for Coq grammar. | |||
| 2018-11-05 | Remove Smeta constructor in Gramlib. | Pierre-Marie Pédrot | |
| This constructor was only used by meta-level macros that are not used and serve no purpose in the grammar engine. | |||
| 2018-11-04 | Remove the deprecated Token module and port the corresponding code. | Pierre-Marie Pédrot | |
| 2018-10-29 | [gramlib] Wrap `Gramlib`. | Emilio Jesus Gallego Arias | |
| This introduces a bit of noise in the Dune files but for now I think it is the best way to do it. | |||
| 2018-10-29 | [gramlib] Cleanup, remove unused parsing infrastructure. | Emilio Jesus Gallego Arias | |
| We remove the functional and backtracking parsers as they are not used in Coq. | |||
| 2018-10-29 | [camlp5] Fix warnings, switch Coq to vendored library. | Emilio Jesus Gallego Arias | |
| 2018-10-29 | [camlp5] Automatic conversion from revised syntax + parsers | Emilio Jesus Gallego Arias | |
| `for i in *; do camlp5r pr_o.cmo $i > ../gramlib.auto/$i; done` | |||
| 2018-10-29 | [gramlib] Original Import from Camlp5 repos. | Emilio Jesus Gallego Arias | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |