aboutsummaryrefslogtreecommitdiff
path: root/pretyping/retyping.ml
AgeCommit message (Expand)Author
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-04-01Actually exporting delayed universes in the EConstr implementation.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Eliminating parts of the right-hand side compatibility layerPierre-Marie Pédrot
2017-02-14Leminv API using EConstr.Pierre-Marie Pédrot
2017-02-14Cleaning up opening of the EConstr module in pretyping folder.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-11-25Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej).Hugo Herbelin
2015-11-24Fixing an old typo in Retyping, found by Matej.Hugo Herbelin
2015-07-09Make retyping of projections more resilient to wrong environment.Maxime Dénès
2015-07-05Fix handling of primitive projections in VM.Maxime Dénès
2015-02-27Taking current env and not global env in b286c9f4f42f (4 commits ago,Hugo Herbelin
2015-02-27Add support so that the type of a match in an inductive type with let-inHugo Herbelin
2015-01-12Update headers.Maxime Dénès
2014-10-02Work around issues with FO unification trying to unify terms ofMatthieu Sozeau
2014-10-01Fixing use of arguments renaming in apply which was broken afterHugo Herbelin
2014-09-27Make pattern_of_constr typed so that we can infer the proper patternsMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-18Fix constrMatching as well as change/e_contextually to allowMatthieu Sozeau
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-06-28Quickly fixing bug #2996: typing functions now check when referring toHugo Herbelin
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-01Use of "H"-based names for propositional hypotheses obtained byHugo Herbelin
2014-05-06- Fix arity handling in retyping (de Bruijn bug!)Matthieu Sozeau
2014-05-06Allow records whose sort is defined by a constant.Matthieu Sozeau
2014-05-06Fix interface for template polymorphism, cleaning up code in all typing algor...Matthieu Sozeau
2014-05-06Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Matthieu Sozeau
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-07-19- Fix uncaught exception NotASort from reductionops, moving decomp_sort to re...msozeau
2013-05-14Delayed the computation of parameters in sort polymorphism ofherbelin
2013-05-05Hack to solve a "Bad recursive type" anomaly.herbelin
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-17Retyping.get_type_of: a lax version raising no anomaliesletouzey
2013-02-05Fixed bug #2981 (anomaly NotASort in Retyping due to collision betweenherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 16:27:37 +0000