aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/retyping.ml
Commit message (Expand)AuthorAge
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* [econstr] Forbid calling `to_constr` in open terms.Gravatar Emilio Jesus Gallego Arias2018-03-31
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
* Adding a variant get_truncation_family_of of get_sort_family_of.Gravatar Hugo Herbelin2017-11-28
* Moving non-recursive function sort_family_of out of the retype block of recur...Gravatar Hugo Herbelin2017-11-28
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Remove trivial TODO comment (constants can't be template poly now).Gravatar Gaëtan Gilbert2017-09-28
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
* Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Cleaning up opening of the EConstr module in pretyping folder.Gravatar Pierre-Marie Pédrot2017-02-14
* Making judgment type generic over the type of inner constrs.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
* CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* 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
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej).Gravatar Hugo Herbelin2015-11-25
* Fixing an old typo in Retyping, found by Matej.Gravatar Hugo Herbelin2015-11-24
* Make retyping of projections more resilient to wrong environment.Gravatar Maxime Dénès2015-07-09
* Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
* Taking current env and not global env in b286c9f4f42f (4 commits ago,Gravatar Hugo Herbelin2015-02-27
* Add support so that the type of a match in an inductive type with let-inGravatar Hugo Herbelin2015-02-27
* Update headers.Gravatar Maxime Dénès2015-01-12
* Work around issues with FO unification trying to unify terms ofGravatar Matthieu Sozeau2014-10-02
* Fixing use of arguments renaming in apply which was broken afterGravatar Hugo Herbelin2014-10-01
* Make pattern_of_constr typed so that we can infer the proper patternsGravatar Matthieu Sozeau2014-09-27
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Fix constrMatching as well as change/e_contextually to allowGravatar Matthieu Sozeau2014-09-18
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
* Quickly fixing bug #2996: typing functions now check when referring toGravatar Hugo Herbelin2014-06-28
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Use of "H"-based names for propositional hypotheses obtained byGravatar Hugo Herbelin2014-06-01
* - Fix arity handling in retyping (de Bruijn bug!)Gravatar Matthieu Sozeau2014-05-06
* Allow records whose sort is defined by a constant.Gravatar Matthieu Sozeau2014-05-06
* Fix interface for template polymorphism, cleaning up code in all typing algor...Gravatar Matthieu Sozeau2014-05-06
* Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 16:53:46 +0000