Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | * | | | Fix bug #5476: Ltac has an inconsistent view of hypotheses. | Pierre-Marie Pédrot | 2017-04-19 | |
| |_|/ / / |/| | | | | ||||
* | | | | | Merge PR#573: [toplevel] Fix printing of parsing errors + corner case. | Maxime Dénès | 2017-04-19 | |
|\ \ \ \ \ | ||||
* | | | | | | CHANGES entry for #545. | Maxime Dénès | 2017-04-19 | |
* | | | | | | Merge PR#545: Add some hints to the "real" database to automatically discharg... | Maxime Dénès | 2017-04-19 | |
|\ \ \ \ \ \ | ||||
| | | * \ \ \ | Merge PR#538: Correction of bug #4306 | Maxime Dénès | 2017-04-19 | |
| | | |\ \ \ \ | ||||
* | | | \ \ \ \ | Merge PR#570: Adding and fixing links in README. | Maxime Dénès | 2017-04-19 | |
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR#571: [toplevel] Fix #5475 | Maxime Dénès | 2017-04-19 | |
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / |/| | | | | | | | | ||||
| | | | * | | | | | [toplevel] Fix printing of parsing errors + corner case. | Emilio Jesus Gallego Arias | 2017-04-19 | |
| |_|_|/ / / / / |/| | | | | | | | ||||
| * | | | | | | | [toplevel] Fix #5475 | Emilio Jesus Gallego Arias | 2017-04-18 | |
|/ / / / / / / | ||||
| * / / / / / | Adding and fixing links in README. | Théo Zimmermann | 2017-04-18 | |
|/ / / / / / | ||||
* | | | | | | Add a test for bug #5321: clearbody breaks typing of goal. | Pierre-Marie Pédrot | 2017-04-17 | |
* | | | | | | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-04-15 | |
|\ \ \ \ \ \ | | |/ / / / | |/| | | | | ||||
* | | | | | | Merge PR#523: [readme] Add badges for Travis and Gitter. | Maxime Dénès | 2017-04-15 | |
|\ \ \ \ \ \ | ||||
| | * | | | | | Fixing bug #5470 (anomaly on notations with misused "binder" type). | Hugo Herbelin | 2017-04-14 | |
| | * | | | | | Fixing bug #5469 (notation format not recognizing curly braces). | Hugo Herbelin | 2017-04-14 | |
| | * | | | | | Fix EOL characters in xml protocol documentation. | Maxime Dénès | 2017-04-14 | |
| | * | | | | | Merge PR#556: Fix anomaly when doing [all:Check _.] during a proof. | Maxime Dénès | 2017-04-14 | |
| | |\ \ \ \ \ | ||||
| | | * | | | | | Fix anomaly when doing [all:Check _.] during a proof. | Gaetan Gilbert | 2017-04-14 | |
* | | | | | | | | 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 |