| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-17 | Merge PR#633: An extension of EXTEND and notations to make standard parsing ↵ | Maxime Dénès | |
| tricks available to users | |||
| 2017-05-17 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-05-16 | Adding support for using grammar entries returning no value in EXTEND. | Hugo Herbelin | |
| 2017-05-10 | Switch bedrock to mit-plv base | Jason Gross | |
| 2017-05-08 | Fix warnings in top_printers | Gaetan Gilbert | |
| Note that [@@@ocaml.warning "-32"] caused an error with Drop. It was put there because I didn't realise the warning was about a real issue. | |||
| 2017-05-02 | Merge PR#582: Fix warnings | Maxime Dénès | |
| 2017-05-01 | Add bmsherman/topology to the ci | Jason Gross | |
| This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk. | |||
| 2017-05-01 | More consistent writing of de Bruijn. | Théo Zimmermann | |
| 2017-05-01 | Fix for bug 5507. Mispelt de Bruijn. | Théo Zimmermann | |
| 2017-04-27 | Remove unused [open] statements | Gaetan Gilbert | |
| 2017-04-27 | Locally disable some warnings. | Gaetan Gilbert | |
| 2017-04-27 | Merge PR#568: Remove tactic compatibility layer | Maxime Dénès | |
| 2017-04-27 | Document the API changes. | Pierre-Marie Pédrot | |
| 2017-04-27 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-04-25 | [located] [doc] Improve docs for `CAst.ast`. | Emilio Jesus Gallego Arias | |
| 2017-04-25 | [travis] mathcomp and fiat overlay for #402 | Emilio Jesus Gallego Arias | |
| 2017-04-25 | [location] Document changes. | Emilio Jesus Gallego Arias | |
| 2017-04-25 | [location] Remove `Loc.internal_ghost` | Emilio Jesus Gallego Arias | |
| `internal_ghost` was an artifact to ease porting of the ml4 rules. Now that the location is optional we can finally get rid of it. | |||
| 2017-04-25 | [location] Remove Loc.ghost. | Emilio Jesus Gallego Arias | |
| Now it is a private field, locations are optional. | |||
| 2017-04-24 | [location] Switch glob_constr to Loc.located | Emilio Jesus Gallego Arias | |
| 2017-04-24 | Adding a dedicated travis overlay for fiat-parsers. | Pierre-Marie Pédrot | |
| 2017-04-20 | Add bedrock targets src and facade | Jason Gross | |
| 2017-04-19 | Documenting EConstr for developpers. | Pierre-Marie Pédrot | |
| 2017-04-15 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-04-14 | Fix EOL characters in xml protocol documentation. | Maxime Dénès | |
| 2017-04-14 | Merge PR#563: add XML protocol doc for 8.6 | Maxime Dénès | |
| 2017-04-14 | [travis] Use the lite target for fiat-crypto. | Maxime Dénès | |
| 2017-04-13 | update XML protocol doc to 8.6 | Paul Steckler | |
| 2017-04-13 | add XML protocol doc for 8.5 | Paul Steckler | |
| 2017-04-12 | Merge PR#441: Port Toplevel to the Stm API | Maxime Dénès | |
| 2017-04-12 | [stm] Improve error messages on add/parse. | Emilio Jesus Gallego Arias | |
| As suggested by @psteckler in #524 , we give more explicit information about what is wrong. We also provide some debug information for the possible dangerous case of having the tip go out of sync with the real installed state (which will make parsing fail if there was some changes to the parser). We also fix a couple of typos noticed by Paul, thanks Paul. | |||
| 2017-04-12 | [stm] Port the toplevel to the STM. | Emilio Jesus Gallego Arias | |
| - We clean-up `Vernac` and make it use the STM API. - Now functions in `Vernac` for use in the toplevel and compiler take an starting `Stateid.t`. - Duplicated `Stm.interp` entry point is removed. - The XML protocol call `interp` is disabled. | |||
| 2017-04-12 | [stm] Move main parsing entry point to the STM. | Emilio Jesus Gallego Arias | |
| Mainly due to notations, proof modes and plugins, parsing in Coq is stateful, so we expose a state-aware parsing API in the STM. This is a first move to unify all the parsing entry points in the Stm and the toplevel, and allows STM clients to control their input stream properly. This greatly helps for instance, with whole-document parsing. This commit supersedes PR#204. | |||
| 2017-04-12 | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵ | Maxime Dénès | |
| record fields. | |||
| 2017-04-11 | Merge PR#379: Introducing evar-insensitive constrs | Maxime Dénès | |
| 2017-04-07 | Merge PR#461: [camlpX] Remove camlp4 compat layer. | Maxime Dénès | |
| 2017-04-07 | Fixes for Drop. to work (decl_mode removal and toplevel -> vernac) | Matthieu Sozeau | |
| 2017-04-07 | Merge branch 'master' into econstr | Pierre-Marie Pédrot | |
| 2017-04-07 | [travis] Overlay for PR#461: Camlp4 removal. | Emilio Jesus Gallego Arias | |
| 2017-04-06 | Adding a documentation for the new proof engine. | Pierre-Marie Pédrot | |
| 2017-04-04 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-04-03 | Fix loading of ocamldebug printers. | Pierre-Marie Pédrot | |
| 2017-04-03 | Merge PR#417: No cast surgery in let in | Maxime Dénès | |
| 2017-03-25 | Mathcomp overlay. | Maxime Dénès | |
| 2017-03-24 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-03-24 | [travis] Backport from trunk: VST | Emilio Jesus Gallego Arias | |
| 2017-03-24 | [travis] Add VST | Emilio Jesus Gallego Arias | |
| 2017-03-24 | Documenting main changes of API. | Hugo Herbelin | |
| 2017-03-23 | Improving the API of constrexpr_ops.mli. | Hugo Herbelin | |
| Deprecating abstract_constr_expr in favor of mkCLambdaN, prod_constr_expr in favor of mkCProdN. Note: They did not do exactly the same, the first ones were interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones were preserving the original sharing of the type, what I think is the correct thing to do. So, there is also a "fix" of semantic here. | |||
| 2017-03-23 | Merge PR#501: [travis] Fix iris-coq build. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |