aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/retyping.ml
Commit message (Expand)AuthorAge
* 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
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* - Fix uncaught exception NotASort from reductionops, moving decomp_sort to re...Gravatar msozeau2013-07-19
* Delayed the computation of parameters in sort polymorphism ofGravatar herbelin2013-05-14
* Hack to solve a "Bad recursive type" anomaly.Gravatar herbelin2013-05-05
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Retyping.get_type_of: a lax version raising no anomaliesGravatar letouzey2013-03-17
* Fixed bug #2981 (anomaly NotASort in Retyping due to collision betweenGravatar herbelin2013-02-05
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 04:54:16 +0000