aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/coercion.ml
Commit message (Expand)AuthorAge
* Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Evardefine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Program: cleanup in cases, add optionsGravatar Matthieu Sozeau2016-06-29
* Rework treatment of default transparency of obligationsGravatar Matthieu Sozeau2016-06-27
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\
| * More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).Gravatar Hugo Herbelin2016-06-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\|
| * Fix a bug in Program coercion codeGravatar Matthieu Sozeau2016-03-25
* | Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
* | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \
* | | Renaming functions in Typing to stick to the standard e_* scheme.Gravatar Pierre-Marie Pédrot2016-02-15
| |/ |/|
| * CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fix bug #3998: when using typeclass resolution for conversion, allowGravatar Matthieu Sozeau2015-11-11
* Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.Gravatar Hugo Herbelin2015-07-10
* Make Coercion.inh_app_fun respect its specification.Gravatar Pierre-Marie Pédrot2015-05-15
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Setup hook to change the unification algorithm used by evarconv,Gravatar Matthieu Sozeau2014-12-09
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* A few Global.env removed.Gravatar Hugo Herbelin2014-10-04
* Fix bug #3672, application of primitive projections as coercions.Gravatar Matthieu Sozeau2014-09-27
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Use kernel conversion on terms that contain universe variables during unifica...Gravatar Matthieu Sozeau2014-07-20
* Fix coercion code to disallow using cumulativity in the domain of products, w...Gravatar Matthieu Sozeau2014-07-17
* Add an option to disable typeclass resolution during conversion, whichGravatar Matthieu Sozeau2014-06-26
* Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead of...Gravatar Matthieu Sozeau2014-06-13
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* Keep track of universes on coercion applications even if they're not polymorp...Gravatar Matthieu Sozeau2014-05-06
* Correct universe handling in program coercions (bug #2378).Gravatar Matthieu Sozeau2014-05-06
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* TC: honor the use_typeclasses flag in pretypingGravatar Enrico Tassi2014-02-12
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Removing almost all new_untyped_evar, and a bunch of Evd.add.Gravatar ppedrot2013-09-18
* Uniformization: isevars -> evdref/sigma/evdGravatar herbelin2013-05-09
* Small cleaning of Evd interface.Gravatar ppedrot2013-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 12:03:48 +0000