| Commit message (Expand) | Author | Age |
* | Deprecate Typing.e_* functions | Gaëtan Gilbert | 2018-05-14 |
* | Deprecate Refiner [evar_map ref] exported functions. | Gaëtan Gilbert | 2018-05-14 |
* | [api] Rename `global_reference` to `GlobRef.t` to follow kernel style. | Emilio Jesus Gallego Arias | 2018-05-04 |
* | [api] Move bullets and goals selectors to `proofs/` | Emilio Jesus Gallego Arias | 2018-05-01 |
* | Strict focusing using Default Goal Selector. | Gaëtan Gilbert | 2018-04-29 |
* | Merge PR #7108: Legacy refiner handle eta-expanded case analysis | Pierre-Marie Pédrot | 2018-04-23 |
|\ |
|
* | | Evar maps contain econstrs. | Gaëtan Gilbert | 2018-04-13 |
| * | Preparing old-style refine from logic.ml to deal with "Cases" proof | Hugo Herbelin | 2018-03-29 |
* | | Congruence: getting rid of a detour by the compatibility layer of proof engine. | Hugo Herbelin | 2018-03-27 |
|/ |
|
* | [located] More work towards using CAst.t | Emilio Jesus Gallego Arias | 2018-03-09 |
* | Cosmetic: add an expected newline in proof_global. | Hugo Herbelin | 2018-03-08 |
* | Add an invariant on future goals in Proof.run_tactic. | Hugo Herbelin | 2018-03-08 |
* | Proof engine: support for nesting tactic-in-term within other tactics. | Hugo Herbelin | 2018-03-08 |
* | Proof engine: using save_future_goal when relevant. | Hugo Herbelin | 2018-03-08 |
* | Proof engine: consider the pair principal and future goals as an entity. | Hugo Herbelin | 2018-03-08 |
* | Rename some universe minimizing "normalize" functions to "minimize" | Gaëtan Gilbert | 2018-03-06 |
* | Deprecate UState aliases in Evd. | Gaëtan Gilbert | 2018-03-06 |
* | Merge PR #6855: Update headers following #6543. | Maxime Dénès | 2018-03-05 |
|\ |
|
* \ | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`. | Maxime Dénès | 2018-03-04 |
|\ \ |
|
* \ \ | Merge PR #6676: [proofview] goals come with a state | Maxime Dénès | 2018-03-04 |
|\ \ \ |
|
| | * | | [econstr] Continue consolidation of EConstr API under `interp`. | Emilio Jesus Gallego Arias | 2018-02-28 |
| |/ /
|/| | |
|
| | * | Update headers following #6543. | Théo Zimmermann | 2018-02-27 |
| |/
|/| |
|
* | | [ast] Improve precision of Ast location recognition in serialization. | Emilio Jesus Gallego Arias | 2018-02-22 |
| * | proofview: goals come with a state | Enrico Tassi | 2018-02-20 |
|/ |
|
* | Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t` | Maxime Dénès | 2018-02-19 |
|\ |
|
* | | [toplevel] Make toplevel state into a record. | Emilio Jesus Gallego Arias | 2018-02-15 |
| * | [engine] Remove ghost parameter from `Proofview.Goal.t` | Emilio Jesus Gallego Arias | 2018-02-12 |
|/ |
|
* | Reductionops.nf_* now take an environment. | Gaëtan Gilbert | 2018-02-02 |
* | Fix #6591: anomaly when using selectors outside of a proof. | Cyprien Mangin | 2018-01-22 |
* | Force polymorphic definitions to have no internal constraints. | Pierre-Marie Pédrot | 2018-01-11 |
* | Merge PR #6264: [kernel] Patch allowing to disable VM reduction. | Maxime Dénès | 2017-12-14 |
|\ |
|
* \ | Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind. | Maxime Dénès | 2017-12-14 |
|\ \ |
|
* | | | [proof] Embed evar_map in RefinerError exception. | Emilio Jesus Gallego Arias | 2017-12-11 |
* | | | Merge PR #6368: [api] Remove yet another type alias. | Maxime Dénès | 2017-12-11 |
|\ \ \ |
|
* \ \ \ | Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract. | Maxime Dénès | 2017-12-11 |
|\ \ \ \ |
|
| | * | | | [api] Remove yet another type alias. | Emilio Jesus Gallego Arias | 2017-12-09 |
| | | * | | [lib] Rename Profile to CProfile | Emilio Jesus Gallego Arias | 2017-12-09 |
| | |/ / |
|
* | / / | Remove up-to-conversion matching functions. | Pierre-Marie Pédrot | 2017-12-09 |
| |/ /
|/| | |
|
| * | | Fix #6323: stronger restrict universe context vs abstract. | Gaëtan Gilbert | 2017-12-06 |
|/ / |
|
| * | [kernel] Patch allowing to disable VM reduction. | Emilio Jesus Gallego Arias | 2017-12-02 |
* | | Cleanup API for registering universe binders. | Matthieu Sozeau | 2017-12-01 |
|/ |
|
* | [proof] [api] Rename proof types in preparation for functionalization. | Emilio Jesus Gallego Arias | 2017-11-29 |
* | Merge PR #1033: Universe binder improvements | Maxime Dénès | 2017-11-28 |
|\ |
|
* | | [api] Remove aliases of `Evar.t` | Emilio Jesus Gallego Arias | 2017-11-26 |
| * | Make restrict_universe_context stronger. | Gaëtan Gilbert | 2017-11-25 |
| * | In close_proof only check univ decls with the restricted context. | 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 |
|/ |
|