aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typing.ml
AgeCommit message (Expand)Author
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-11Update various comments to use "template polymorphism"Gaetan Gilbert
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-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Evar-normalizing functions now act on EConstrs.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.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-14Clenv 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-14Typing API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarconv API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarsolve API using EConstr.Pierre-Marie Pédrot
2017-02-14Evardefine API using EConstr.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2016-09-14Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-14Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-10Fixing #5077 (failure on typing a fixpoint with evars in its type).Hugo Herbelin
2016-08-10Make it a bit more obvious when variables are of type unit.Guillaume Melquiond
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-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-16Factorizing the uses of Declareops.safe_flags.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-03-20Splitting Evarutil in two distinct files.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Renaming functions in Typing to stick to the standard e_* scheme.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-31Merge branch 'v8.5' into trunkGuillaume Melquiond
2015-12-17(Partial) fix for bug #4453: raise an error instead of an anomaly.Matthieu Sozeau
2015-12-15Fixing unexpected length of context in a typing function, detected byHugo Herbelin
2015-12-05Unifying betazeta_applist and prod_applist into a clearer interface.Hugo Herbelin
2015-06-26Add a flag to deactivate guard checking in the kernel.Arnaud Spiwack
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-10-20Fixing a bug in the presence of let-in in inductive arity.Hugo Herbelin
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-09-04Proofview refiner is now type-safe by default.Pierre-Marie Pédrot
2014-09-04Typing.sort_of does not leak evarmaps anymore.Pierre-Marie Pédrot
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-06-28Quickly fixing bug #2996: typing functions now check when referring toHugo Herbelin
2014-06-26Change interface of refresh universes to get a pbty argument instead ofMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:32:17 +0000