Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | | | Merge PR#557: [toplevel] Don't print goals if there is no pending proof. | Maxime Dénès | 2017-04-14 | |
|\ \ \ \ \ \ | ||||
* \ \ \ \ \ \ | Merge PR#554: Update INSTALL now that -debug is the default. | 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-14 | |
| | | | | |/ / / | | | | |/| | | | ||||
* | | | | | | | | Merge PR#559: Fix compilation with camlp5 transitional mode. | Maxime Dénès | 2017-04-14 | |
|\ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | Fix compilation with camlp5 transitional mode. | Maxime Dénès | 2017-04-14 | |
|/ / / / / / / / | ||||
| | | | | * | | | update XML protocol doc to 8.6 | Paul Steckler | 2017-04-13 | |
| | | | | * | | | add XML protocol doc for 8.5 | Paul Steckler | 2017-04-13 | |
| | | | |/ / / | ||||
| | * | | | | | [toplevel] Don't print goals if there is no pending proof. | Emilio Jesus Gallego Arias | 2017-04-13 | |
* | | | | | | | Silence a few OCaml warnings. | Guillaume Melquiond | 2017-04-13 | |
| |/ / / / / |/| | | | | | ||||
| | | * | | | Merge PR#510: Correctly identify [Time Defined.] as a defined | Maxime Dénès | 2017-04-12 | |
| | | |\ \ \ | ||||
* | | | \ \ \ | Merge PR#441: Port Toplevel to the Stm API | Maxime Dénès | 2017-04-12 | |
|\ \ \ \ \ \ \ | ||||
| * | | | | | | | [toplevel] [stm] cleanup in module open | Emilio Jesus Gallego Arias | 2017-04-12 | |
| * | | | | | | | [stm] [nit] Centralize compile-time debug flag. | Emilio Jesus Gallego Arias | 2017-04-12 | |
| * | | | | | | | [stm] Improve error messages on add/parse. | Emilio Jesus Gallego Arias | 2017-04-12 | |
| * | | | | | | | [flags] Documentation and a minor tweak. | Emilio Jesus Gallego Arias | 2017-04-12 | |
| * | | | | | | | [vernac] vernacentries.mli cleanup | Emilio Jesus Gallego Arias | 2017-04-12 | |
| * | | | | | | | [stm] Port the toplevel to the STM. | Emilio Jesus Gallego Arias | 2017-04-12 | |
| * | | | | | | | [stm] Move main parsing entry point to the STM. | Emilio Jesus Gallego Arias | 2017-04-12 | |
| * | | | | | | | [stm] Remove edit_id. | Emilio Jesus Gallego Arias | 2017-04-12 | |
* | | | | | | | | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r... | Maxime Dénès | 2017-04-12 | |
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR#549: Fast path in weak head reduction of applied atoms. | Maxime Dénès | 2017-04-11 | |
|\ \ \ \ \ \ \ \ \ | ||||
| | | | * | | | | | | Update INSTALL now that -debug is the default. | Théo Zimmermann | 2017-04-11 | |
| |_|_|/ / / / / / |/| | | | | | | | | ||||
* | | | | | | | | | Merge PR#543: Sanitize instance interpretation | Maxime Dénès | 2017-04-11 | |
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR#532: Clean Nsatz implementation. | Maxime Dénès | 2017-04-11 | |
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR#537: Efficient side-effect abstraction | Maxime Dénès | 2017-04-11 | |
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR#379: Introducing evar-insensitive constrs | Maxime Dénès | 2017-04-11 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | | | Adding a test for 'rewrite in *' when an evar is solved by side-effect. | Pierre-Marie Pédrot | 2017-04-10 | |
| * | | | | | | | | | | | | Adding a test for the correctness of normalization in legacy typeclasses. | Pierre-Marie Pédrot | 2017-04-10 | |
| * | | | | | | | | | | | | Documenting the changes introduced by the EConstr branch. | Pierre-Marie Pédrot | 2017-04-10 | |
* | | | | | | | | | | | | | Revert "refactoring: Reductionops.contextual_reduction_function type" | Matej Košík | 2017-04-10 | |
* | | | | | | | | | | | | | Revert "comment: typo" | Matej Košík | 2017-04-10 | |
* | | | | | | | | | | | | | Revert "refactoring: Names.DirPath.equal" | Matej Košík | 2017-04-10 | |
* | | | | | | | | | | | | | Revert "refactoring: Names.DirPath.compare" | Matej Košík | 2017-04-10 | |
* | | | | | | | | | | | | | Revert "refactoring: Names.DirPath.is_empty" | Matej Košík | 2017-04-10 | |
* | | | | | | | | | | | | | Revert "simplify: Environ.push_named" | Matej Košík | 2017-04-10 | |
* | | | | | | | | | | | | | Revert "trivial" | Matej Košík | 2017-04-10 | |
* | | | | | | | | | | | | | Revert "trivial" | Matej Košík | 2017-04-10 | |
* | | | | | | | | | | | | | Revert "comments: corrected in the Context module" | Matej Košík | 2017-04-10 | |
* | | | | | | | | | | | | | comments: corrected in the Context module | Matej Kosik | 2017-04-10 | |
* | | | | | | | | | | | | | trivial | Matej Kosik | 2017-04-10 | |
* | | | | | | | | | | | | | trivial | Matej Kosik | 2017-04-10 | |
* | | | | | | | | | | | | | simplify: Environ.push_named | Matej Kosik | 2017-04-10 | |
* | | | | | | | | | | | | | refactoring: Names.DirPath.is_empty | Matej Kosik | 2017-04-10 | |
* | | | | | | | | | | | | | refactoring: Names.DirPath.compare | Matej Kosik | 2017-04-10 | |
* | | | | | | | | | | | | | refactoring: Names.DirPath.equal | Matej Kosik | 2017-04-10 | |
* | | | | | | | | | | | | | comment: typo | Matej Kosik | 2017-04-10 | |
* | | | | | | | | | | | | | refactoring: Reductionops.contextual_reduction_function type | Matej Kosik | 2017-04-10 | |
* | | | | | | | | | | | | | Merge PR#547: [toplevel] Remove the feedback printer only on exit. | Maxime Dénès | 2017-04-10 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#548: [ide] Correctly place warning tags. | Maxime Dénès | 2017-04-10 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |