| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Making detyping potentially lazy. |  Pierre-Marie Pédrot | 2017-09-04 |
| | | | | | | | | | | | | | | | | | | | | The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager. | ||
| * | [api] Remove type equalities from API. |  Emilio Jesus Gallego Arias | 2017-07-25 |
| | | | | | | | | | | | | | This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli` | ||
| * | [API] Remove `open API` in ml files in favor of `-open API` flag. | Emilio Jesus Gallego Arias | 2017-07-17 |
| | | |||
| * | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global. | Pierre-Marie Pédrot | 2017-07-13 |
| | | |||
| * | Remove (useless) aliases from the API. |  Matej Košík | 2017-06-10 |
| | | |||
| * | Put "ssreflect" behind "API". | Matej Košík | 2017-06-07 |
| | | |||
| * | Merge the ssr plugin. |  Maxime Dénès | 2017-06-06 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |