aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typing.ml
AgeCommit message (Expand)Author
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
2014-06-21- Add an option to refresh only algebraic universes, for e_type_of. The goalMatthieu Sozeau
2014-06-20Cleanup treatment of template universe polymorphism (thanks to E. TassiMatthieu Sozeau
2014-05-09Refresh universes for Ltac's type_of, as the term can be used anywhere,Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Fix interface for template polymorphism, cleaning up code in all typing algor...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-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-05-14Delayed the computation of parameters in sort polymorphism ofherbelin
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-02-17A more informative message when the elimination predicate forherbelin
2013-02-10Moved code from Pretype_error to Evarutilppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Taking into account the possibility of having a type of type which isherbelin
2012-11-22Monomorphization (pretyping)ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 17:22:32 +0000