| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-02-19 | Gramlib: Fixes #9358 (ensuring that the loc function has something to compute). | Hugo Herbelin | |
| 2019-02-11 | Almost fully type-safe implementation of camlp5. | Pierre-Marie Pédrot | |
| There are still minute uses of type-unsafe primitives. Most of them can be removed if I had a little higher dan in GADTs (or weeks to spare thinking about how non-interactive proofs can be performed) but one, which is really a potential source of unsoundness. The latter is not problematic as all uses in Coq are protected about the unsoundness proof, but the API is clearly deficient and needs to be fixed at some point. | |||
| 2019-02-11 | Further propagation of well-typedness in Grammar. | Pierre-Marie Pédrot | |
| 2019-02-11 | Introduce a GADT of well-typed grammar entries in Grammar. | Pierre-Marie Pédrot | |
| Not fully used yet, we rely on erasure casts for now. | |||
| 2019-02-11 | Centralizing the calls to the global mutable grammar in Grammar. | Pierre-Marie Pédrot | |
| 2019-02-11 | Specialize the intermediate types of the Grammar functor. | Pierre-Marie Pédrot | |
| Now that we depend on a module argument, we do not have to quantify over the arguments anymore. | |||
| 2019-02-11 | Make Grammar truly functorial. | Pierre-Marie Pédrot | |
| The old implementation was simply hiding the fact that the functor relied on a generic data type. If we want to implement the grammar engine in a truly type-safe way, we need to make the ancilliary datatypes depend on the type parameters. | |||
| 2019-02-11 | Move most of Gramext into Grammar. | Pierre-Marie Pédrot | |
| This module was defining unsafe functions and datatypes only relevant to the grammar engine. We hide them under the API so as to be able to later clean it up. | |||
| 2019-02-11 | Merge PR #9478: Remove the comment fields of locations. | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-02-05 | Remove the Plexing.Error exception. | Pierre-Marie Pédrot | |
| This was dead code, it was never raised ever. | |||
| 2019-02-05 | Remove the comment fields of locations. | Pierre-Marie Pédrot | |
| They didn't seem to be used at all. | |||
| 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 |