| Commit message (Expand) | Author | Age |
* | Getting rid of pf_is_matching in Funind. | Pierre-Marie Pédrot | 2017-12-06 |
* | Merge PR #890: Global universe declarations | Maxime Dénès | 2017-12-05 |
|\ |
|
* \ | Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212 | Maxime Dénès | 2017-12-05 |
|\ \ |
|
* \ \ | Merge PR #6210: More complete not-fully-applied error messages, #6145 | Maxime Dénès | 2017-12-05 |
|\ \ \ |
|
| | | * | Proper nametab handling of global universe names | Matthieu Sozeau | 2017-12-01 |
| |_|/
|/| | |
|
* | | | Remove "obsolete_locality" and fix STM vernac classification. | Maxime Dénès | 2017-11-29 |
| * | | more complete not-fully-applied error messages, #6145 | Paul Steckler | 2017-11-28 |
* | | | Merge PR #1033: Universe binder improvements | Maxime Dénès | 2017-11-28 |
|\ \ \ |
|
* \ \ \ | Merge PR #6248: [api] Remove aliases of `Evar.t` | Maxime Dénès | 2017-11-28 |
|\ \ \ \ |
|
| | | | * | allow :: and , as infix ops | Paul Steckler | 2017-11-27 |
| * | | | | [api] Remove aliases of `Evar.t` | Emilio Jesus Gallego Arias | 2017-11-26 |
* | | | | | Use Evarutil.has_undefined_evars for tactic has_evar. | Gaëtan Gilbert | 2017-11-24 |
|/ / / / |
|
| * | | | Use Entries.constant_universes_entry more. | Gaëtan Gilbert | 2017-11-24 |
| * | | | When declaring constants/inductives use ContextSet if monomorphic. | Gaëtan Gilbert | 2017-11-24 |
| * | | | Stop exposing UState.universe_context and its Evd wrapper. | Gaëtan Gilbert | 2017-11-24 |
| * | | | Separate checking univ_decls and obtaining universe binder names. | Gaëtan Gilbert | 2017-11-24 |
|/ / / |
|
* | | | Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRing | Maxime Dénès | 2017-11-24 |
|\ \ \ |
|
* \ \ \ | Merge PR #486: Make some functions on terms more robust w.r.t new term constr... | Maxime Dénès | 2017-11-24 |
|\ \ \ \ |
|
* \ \ \ \ | Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion | Maxime Dénès | 2017-11-24 |
|\ \ \ \ \ |
|
* \ \ \ \ \ | Merge PR #6197: [plugin] Remove LocalityFixme über hack. | Maxime Dénès | 2017-11-24 |
|\ \ \ \ \ \ |
|
| | | * | | | | Make some functions on terms more robust w.r.t new term constructs. | Maxime Dénès | 2017-11-23 |
* | | | | | | | Merge PR #6186: [api] Miscellaneous consolidation. | Maxime Dénès | 2017-11-23 |
|\ \ \ \ \ \ \
| |_|_|/ / / /
|/| | | | | | |
|
| | | * | | | | Recognizing Z in romega up to conversion. | Hugo Herbelin | 2017-11-23 |
| | | * | | | | Using is_conv rather than eq_constr to find `nat` or `Z` in omega. | Hugo Herbelin | 2017-11-23 |
| |_|/ / / /
|/| | | | | |
|
| | | * | | | Fixing a 8.7 regression of ring_simplify in ArithRing. | Hugo Herbelin | 2017-11-23 |
| |_|/ / /
|/| | | | |
|
* | | | | | Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag. | Maxime Dénès | 2017-11-23 |
|\ \ \ \ \ |
|
| | | * | | | [plugin] Remove LocalityFixme über hack. | Emilio Jesus Gallego Arias | 2017-11-22 |
| |_|/ / /
|/| | | | |
|
| | | | * | allow whitespace around infix op | Paul Steckler | 2017-11-22 |
| | | | * | use OCaml criteria for infix ops, #6212 | Paul Steckler | 2017-11-22 |
| |_|_|/
|/| | | |
|
| | * | | [api] Deprecate Term destructors, move to Constr | Emilio Jesus Gallego Arias | 2017-11-22 |
| | * | | [api] Miscellaneous consolidation + moves to engine. | Emilio Jesus Gallego Arias | 2017-11-21 |
| |/ /
|/| | |
|
* | | | [printing] Deprecate all printing functions accessing the global proof. | Emilio Jesus Gallego Arias | 2017-11-21 |
* | | | Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API. | Maxime Dénès | 2017-11-21 |
|\ \ \ |
|
* \ \ \ | Merge PR #6113: Extra work on ltac printing: fixing #5787, some parentheses | Maxime Dénès | 2017-11-21 |
|\ \ \ \ |
|
| * | | | | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic). | Hugo Herbelin | 2017-11-20 |
* | | | | | Merge PR #6183: [plugins] Prepare plugin API for functional handling of state. | Maxime Dénès | 2017-11-20 |
|\ \ \ \ \ |
|
* \ \ \ \ \ | Merge PR #6161: Fix micromega.ml to match generated file and enforce match in... | Maxime Dénès | 2017-11-20 |
|\ \ \ \ \ \ |
|
| | | | | * | | Fix #5790: make Hint Resolve <- respect univ polymorphism flag. | Gaëtan Gilbert | 2017-11-19 |
| |_|_|_|/ /
|/| | | | | |
|
| | * | | | | [plugins] Prepare plugin API for functional handling of state. | Emilio Jesus Gallego Arias | 2017-11-19 |
| |/ / / /
|/| | | | |
|
| | | * | | [proof] Attempt to deprecate some V82 parts of the proof API. | Emilio Jesus Gallego Arias | 2017-11-19 |
| |_|/ /
|/| | | |
|
* | | | | Merge PR #6148: [api] Another large deprecation, `Nameops` and friends. | Maxime Dénès | 2017-11-16 |
|\ \ \ \ |
|
* \ \ \ \ | Merge PR #6023: Use GHC.Base.Any for compatibility with GHC 8.2 | Maxime Dénès | 2017-11-16 |
|\ \ \ \ \
| |_|_|_|/
|/| | | | |
|
| | | * | | Fix micromega.ml to match generated file and enforce match in make. | Gaëtan Gilbert | 2017-11-16 |
| |_|/ /
|/| | | |
|
| | | * | Fixing printing of tactics encapsulated as tacarg with Tacexp. | Hugo Herbelin | 2017-11-15 |
| | | * | Using "l" printer for glob_constr, like for constr. | Hugo Herbelin | 2017-11-15 |
| |_|/
|/| | |
|
| | * | [api] Another large deprecation, `Nameops` | Emilio Jesus Gallego Arias | 2017-11-13 |
| |/
|/| |
|
* | | Merge PR #6098: [api] Move structures deprecated in the API to the core. | Maxime Dénès | 2017-11-13 |
|\ \ |
|
| * | | [api] Move structures deprecated in the API to the core. | Emilio Jesus Gallego Arias | 2017-11-06 |
* | | | Adding support for syntax "let _ := e in e'" in Ltac. | Hugo Herbelin | 2017-11-04 |
|/ / |
|
* | | Merge PR #6047: A generic printer for ltac values | Maxime Dénès | 2017-11-03 |
|\ \ |
|