| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-11 | [coqpp] Move to its own directory. | Emilio Jesus Gallego Arias | |
| Coqpp has nothing to do with `grammar`, we thus place it in its own directory, which will prove convenient in more modular build systems. Note that we add `coqpp` to the list of global includes, we could have indeed added some extra rules, but IMHO not worth it as hopefully proper containment will be soon checked by Dune. | |||
| 2018-07-02 | Remove the hardcoded compatibility wit_hyp -> wit_var from the parser. | Pierre-Marie Pédrot | |
| 2018-07-02 | Implementing TACTIC EXTEND in coqpp. | Pierre-Marie Pédrot | |
| 2018-06-29 | Use 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |