Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | Merge branch v8.6 into trunk | Hugo Herbelin | 2017-04-22 | |
|\ \ \ \ | ||||
| | * | | | Remove VernacError | Gaetan Gilbert | 2017-04-21 | |
| |/ / / |/| | | | ||||
| | * | | [flags] Deprecate is_silent/is_verbose in favor of single flag. | Emilio Jesus Gallego Arias | 2017-04-21 | |
| |/ / |/| | | ||||
| | * | Fix nsatz not recognizing real literals. | Guillaume Melquiond | 2017-04-20 | |
| |/ |/| | ||||
* | | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-04-15 | |
|\ \ | ||||
* | | | Silence a few OCaml warnings. | Guillaume Melquiond | 2017-04-13 | |
* | | | Merge PR#441: Port Toplevel to the Stm API | Maxime Dénès | 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#532: Clean Nsatz implementation. | Maxime Dénès | 2017-04-11 | |
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR#379: Introducing evar-insensitive constrs | Maxime Dénès | 2017-04-11 | |
|\ \ \ \ \ \ | |_|_|/ / / |/| | | | | | ||||
| | * | | | | Fix an algorithmic issue in Nsatz. | Pierre-Marie Pédrot | 2017-04-09 | |
| | * | | | | Academic prescriptivism strikes back: down with baroque programming in Nsatz. | Pierre-Marie Pédrot | 2017-04-09 | |
| |/ / / / |/| | | | | ||||
| * | | | | Fix an unhandled exception in Omega. | Pierre-Marie Pédrot | 2017-04-07 | |
| * | | | | Merge branch 'master' into econstr | Pierre-Marie Pédrot | 2017-04-07 | |
| |\ \ \ \ | ||||
* | | | | | | [camlpX] Remove camlp4 compat layer. | Emilio Jesus Gallego Arias | 2017-04-07 | |
| |/ / / / |/| | | | | ||||
* | | | | | Merge PR#455: Farewell decl_mode | Maxime Dénès | 2017-04-06 | |
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR#508: Optimize pending evars | Maxime Dénès | 2017-04-06 | |
|\ \ \ \ \ \ | ||||
| | | * | | | | Fix a normalization hotspot in computation of constr keys. | Pierre-Marie Pédrot | 2017-04-06 | |
| | | | | | * | end of correction of bug 4306 | Julien Forest | 2017-04-04 | |
| | | | | | * | Bad correction in previous commit | Julien Forest | 2017-04-04 | |
| | | | | | * | Solving first problem in bug #4306. TO DO : solve the let in problem | Julien Forest | 2017-04-04 | |
| | | | | |/ | ||||
| | | * | | | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-04-04 | |
| | | |\ \ \ | |_|_|/ / / |/| | | | | | ||||
* | | | | | | Merge PR#417: No cast surgery in let in | Maxime Dénès | 2017-04-03 | |
|\ \ \ \ \ \ | ||||
| | | | * | | | Using delayed universe instances in EConstr. | Pierre-Marie Pédrot | 2017-04-01 | |
* | | | | | | | Declaring ltac plugin, so that static linking works. | Hugo Herbelin | 2017-04-01 | |
| | | | * | | | Actually exporting delayed universes in the EConstr implementation. | Pierre-Marie Pédrot | 2017-04-01 | |
| | | | * | | | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-03-24 | |
| | | | |\ \ \ | |_|_|_|/ / / |/| | | | | | | ||||
| * | | | | | | Replacing "cast surgery" in LetIn by a proper field (see PR #404). | Hugo Herbelin | 2017-03-24 | |
| * | | | | | | Unifying standard "constr_level" names for constructors of local_binder_expr. | Hugo Herbelin | 2017-03-24 | |
| * | | | | | | Renaming local_binder into local_binder_expr. | Hugo Herbelin | 2017-03-24 | |
| * | | | | | | "Standardizing" the name LocalPatten into LocalRawPattern. | Hugo Herbelin | 2017-03-24 | |
|/ / / / / / | ||||
| | | | * / | Improving the API of constrexpr_ops.mli. | Hugo Herbelin | 2017-03-23 | |
| |_|_|/ / |/| | | | | ||||
* | | | | | Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220." | Maxime Dénès | 2017-03-23 | |
* | | | | | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-03-23 | |
|\ \ \ \ \ | | |_|_|/ | |/| | | | ||||
| * | | | | Merge PR#495: funind: Ignore missing info for current function | Maxime Dénès | 2017-03-23 | |
| |\ \ \ \ | ||||
| | | * | | | Fast path for implicit tactic solving. | Pierre-Marie Pédrot | 2017-03-23 | |
| | | * | | | Ensuring static invariants about handling of pending evars in Pretyping. | Pierre-Marie Pédrot | 2017-03-23 | |
| * | | | | | Add empty Extraction.v and FunInd.v to prepare landing of PR#220. | Maxime Dénès | 2017-03-23 | |
* | | | | | | Mark ring morphisms as opaque. | Guillaume Melquiond | 2017-03-22 | |
* | | | | | | Change the parser and printer so that they use IZR for real constants. | Guillaume Melquiond | 2017-03-22 | |
* | | | | | | Fix broken evaluation strategies for ring and field. | Guillaume Melquiond | 2017-03-22 | |
* | | | | | | Remove duplicate lemmas. | Guillaume Melquiond | 2017-03-22 | |
| |_|/ / / |/| | | | | ||||
| | * | | | funind: Ignore missing info for current function | Tej Chajed | 2017-03-22 | |
| |/ / / | ||||
* | | | | [extraction] Flush formatters at end of output. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | | [pp] Move terminal-specific tagging to the toplevel. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | | [pp] Make feedback the only logging mechanism. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | | [pp] Force well-formed boxes by construction. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | | [pp] Prepare for serialization, remove opaque glue. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | | [pp] Remove `Pp.stras`. | Emilio Jesus Gallego Arias | 2017-03-21 |