| Commit message (Expand) | Author | Age |
* | Actually exporting delayed universes in the EConstr implementation. | Pierre-Marie Pédrot | 2017-04-01 |
* | Definining EConstr-based contexts. | Pierre-Marie Pédrot | 2017-02-14 |
* | Evar-normalizing functions now act on EConstrs. | Pierre-Marie Pédrot | 2017-02-14 |
* | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | 2017-02-14 |
* | Removing compatibility layers in Retyping | Pierre-Marie Pédrot | 2017-02-14 |
* | Reductionops now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 |
* | Eliminating parts of the right-hand side compatibility layer | Pierre-Marie Pédrot | 2017-02-14 |
* | Tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | Cleaning up opening of the EConstr module in pretyping folder. | Pierre-Marie Pédrot | 2017-02-14 |
* | Making judgment type generic over the type of inner constrs. | Pierre-Marie Pédrot | 2017-02-14 |
* | Pretyping API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | Coercion API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | Classops API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | Typing API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | Evarconv API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | Evardefine API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | Retyping API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | Reductionops API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | Termops API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | Merge PR #244. | Pierre-Marie Pédrot | 2016-09-08 |
|\ |
|
* | | CLEANUP: minor readability improvements | Matej Kosik | 2016-08-24 |
| * | Unify location handling of error functions. | Emilio Jesus Gallego Arias | 2016-08-19 |
|/ |
|
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey | 2016-07-03 |
* | Separate flags for fix/cofix/match reduction and clean reduction function names. | Maxime Dénès | 2016-07-01 |
* | Program: cleanup in cases, add options | Matthieu Sozeau | 2016-06-29 |
* | Rework treatment of default transparency of obligations | Matthieu Sozeau | 2016-06-27 |
* | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-06-27 |
|\ |
|
| * | More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause). | Hugo Herbelin | 2016-06-27 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-03-30 |
|\| |
|
| * | Fix a bug in Program coercion code | Matthieu Sozeau | 2016-03-25 |
* | | Splitting Evarutil in two distinct files. | Pierre-Marie Pédrot | 2016-03-20 |
* | | merging conflicts with the original "trunk__CLEANUP__Context__2" branch | Matej Kosik | 2016-02-15 |
|\ \ |
|
* | | | Renaming functions in Typing to stick to the standard e_* scheme. | Pierre-Marie Pédrot | 2016-02-15 |
| |/
|/| |
|
| * | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik | 2016-02-09 |
|/ |
|
* | Update copyright headers. | Maxime Dénès | 2016-01-20 |
* | Fix bug #3998: when using typeclass resolution for conversion, allow | Matthieu Sozeau | 2015-11-11 |
* | Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72. | Hugo Herbelin | 2015-07-10 |
* | Make Coercion.inh_app_fun respect its specification. | Pierre-Marie Pédrot | 2015-05-15 |
* | Safer typing primitives. | Pierre-Marie Pédrot | 2015-05-13 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | Setup hook to change the unification algorithm used by evarconv, | Matthieu Sozeau | 2014-12-09 |
* | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | 2014-12-09 |
* | A few Global.env removed. | Hugo Herbelin | 2014-10-04 |
* | Fix bug #3672, application of primitive projections as coercions. | Matthieu Sozeau | 2014-09-27 |
* | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
* | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin | 2014-09-13 |
* | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin | 2014-09-12 |
* | Use kernel conversion on terms that contain universe variables during unifica... | Matthieu Sozeau | 2014-07-20 |
* | Fix coercion code to disallow using cumulativity in the domain of products, w... | Matthieu Sozeau | 2014-07-17 |
* | Add an option to disable typeclass resolution during conversion, which | Matthieu Sozeau | 2014-06-26 |