Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Removing trivial compatibility layer in omega. | 2017-04-24 | |
* | Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag. | 2017-04-24 | |
|\ | |||
* \ | Merge PR#565: Remove VernacError | 2017-04-24 | |
|\ \ | |||
* \ \ | Merge branch v8.6 into trunk | 2017-04-22 | |
|\ \ \ | |||
| | * | | Remove VernacError | 2017-04-21 | |
| |/ / |/| | | |||
| | * | [flags] Deprecate is_silent/is_verbose in favor of single flag. | 2017-04-21 | |
| |/ |/| | |||
* | | Merge branch 'v8.6' into trunk | 2017-04-15 | |
|\ \ | |||
* | | | Silence a few OCaml warnings. | 2017-04-13 | |
* | | | Merge PR#441: Port Toplevel to the Stm API | 2017-04-12 | |
|\ \ \ | |||
| * | | | [stm] Remove edit_id. | 2017-04-12 | |
* | | | | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r... | 2017-04-12 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR#532: Clean Nsatz implementation. | 2017-04-11 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR#379: Introducing evar-insensitive constrs | 2017-04-11 | |
|\ \ \ \ \ \ | |_|_|/ / / |/| | | | | | |||
| | * | | | | Fix an algorithmic issue in Nsatz. | 2017-04-09 | |
| | * | | | | Academic prescriptivism strikes back: down with baroque programming in Nsatz. | 2017-04-09 | |
| |/ / / / |/| | | | | |||
| * | | | | Fix an unhandled exception in Omega. | 2017-04-07 | |
| * | | | | Merge branch 'master' into econstr | 2017-04-07 | |
| |\ \ \ \ | |||
* | | | | | | [camlpX] Remove camlp4 compat layer. | 2017-04-07 | |
| |/ / / / |/| | | | | |||
* | | | | | Merge PR#455: Farewell decl_mode | 2017-04-06 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR#508: Optimize pending evars | 2017-04-06 | |
|\ \ \ \ \ \ | |||
| | | * | | | | Fix a normalization hotspot in computation of constr keys. | 2017-04-06 | |
| | | | | | * | end of correction of bug 4306 | 2017-04-04 | |
| | | | | | * | Bad correction in previous commit | 2017-04-04 | |
| | | | | | * | Solving first problem in bug #4306. TO DO : solve the let in problem | 2017-04-04 | |
| | | | | |/ | |||
| | | * | | | Merge branch 'trunk' into pr379 | 2017-04-04 | |
| | | |\ \ \ | |_|_|/ / / |/| | | | | | |||
* | | | | | | Merge PR#417: No cast surgery in let in | 2017-04-03 | |
|\ \ \ \ \ \ | |||
| | | | * | | | Using delayed universe instances in EConstr. | 2017-04-01 | |
* | | | | | | | Declaring ltac plugin, so that static linking works. | 2017-04-01 | |
| | | | * | | | Actually exporting delayed universes in the EConstr implementation. | 2017-04-01 | |
| | | | * | | | Merge branch 'trunk' into pr379 | 2017-03-24 | |
| | | | |\ \ \ | |_|_|_|/ / / |/| | | | | | | |||
| * | | | | | | Replacing "cast surgery" in LetIn by a proper field (see PR #404). | 2017-03-24 | |
| * | | | | | | Unifying standard "constr_level" names for constructors of local_binder_expr. | 2017-03-24 | |
| * | | | | | | Renaming local_binder into local_binder_expr. | 2017-03-24 | |
| * | | | | | | "Standardizing" the name LocalPatten into LocalRawPattern. | 2017-03-24 | |
|/ / / / / / | |||
| | | | * / | Improving the API of constrexpr_ops.mli. | 2017-03-23 | |
| |_|_|/ / |/| | | | | |||
* | | | | | Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220." | 2017-03-23 | |
* | | | | | Merge branch 'v8.6' into trunk | 2017-03-23 | |
|\ \ \ \ \ | | |_|_|/ | |/| | | | |||
| * | | | | Merge PR#495: funind: Ignore missing info for current function | 2017-03-23 | |
| |\ \ \ \ | |||
| | | * | | | Fast path for implicit tactic solving. | 2017-03-23 | |
| | | * | | | Ensuring static invariants about handling of pending evars in Pretyping. | 2017-03-23 | |
| * | | | | | Add empty Extraction.v and FunInd.v to prepare landing of PR#220. | 2017-03-23 | |
* | | | | | | Mark ring morphisms as opaque. | 2017-03-22 | |
* | | | | | | Change the parser and printer so that they use IZR for real constants. | 2017-03-22 | |
* | | | | | | Fix broken evaluation strategies for ring and field. | 2017-03-22 | |
* | | | | | | Remove duplicate lemmas. | 2017-03-22 | |
| |_|/ / / |/| | | | | |||
| | * | | | funind: Ignore missing info for current function | 2017-03-22 | |
| |/ / / | |||
* | | | | [extraction] Flush formatters at end of output. | 2017-03-21 | |
* | | | | [pp] Move terminal-specific tagging to the toplevel. | 2017-03-21 | |
* | | | | [pp] Make feedback the only logging mechanism. | 2017-03-21 | |
* | | | | [pp] Force well-formed boxes by construction. | 2017-03-21 |