aboutsummaryrefslogtreecommitdiff
path: root/kernel/environ.ml
AgeCommit message (Expand)Author
2018-10-30Remove Environ.set_universes / Typing.enrich_envGaëtan Gilbert
2018-10-30Simplify universe handling in environ constant_type functionsGaëtan Gilbert
2018-10-16Simplify vars_of_global usageGaëtan Gilbert
2018-10-16Simplify fresh_foo_instance functions and pretyping of univ instanceGaëtan Gilbert
2018-10-16Deprecate Global.universes_of_global (replaced by environ version)Gaëtan Gilbert
2018-10-11A state-free version of is_polymorphic.Hugo Herbelin
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-09-19Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared)Matthieu Sozeau
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-09-14Retroknowledge.KInt31: remove the (unused) group parameterVincent Laporte
2018-09-13Do not catch already declared universes in Environ.add_universesGaëtan Gilbert
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-29Merge PR #7080: Swapping Context and Constr and defining declarations on cons...Maxime Dénès
2018-06-28Make Environ.globals abstract.Gaëtan Gilbert
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-17Getting rid of the const_proj field in the kernel.Pierre-Marie Pédrot
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-05-28Unify pre_env and envMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-23New IR in VM: Clambda.Maxime Dénès
2018-01-23Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for...Maxime Dénès
2018-01-22Merge PR #6506: Fast rel lookupMaxime Dénès
2018-01-20Remove dead code in Environ.Pierre-Marie Pédrot
2018-01-14Store the conversion oracle in constant and inductive definitions.Pierre-Marie Pédrot
2017-12-29Fast environment lookup for rels.Pierre-Marie Pédrot
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-09-28Efficient computation of the names contained in an environment.Pierre-Marie Pédrot
2017-08-12Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.Hugo Herbelin
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-11Safe API for accessing universe constraints of global references.Pierre-Marie Pédrot
2017-07-11Less footguns in universe handling: remove subst_instance_context.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-02-14Introducing contexts parameterized by the inner term type.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
2016-10-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-12Remove dead code in Environ.Pierre-Marie Pédrot
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-09Tracking careless uses of slow name lookup.Pierre-Marie Pédrot
2016-09-09Removing the now useless field env_named_val from named_context_val.Pierre-Marie Pédrot
2016-09-09More efficient implementation of map_named_val.Pierre-Marie Pédrot
2016-09-09Tentative fast-access named envPierre-Marie Pédrot
2016-09-09Packing the named_context_val in a proper record and marking it private.Pierre-Marie Pédrot
2016-08-25CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Matej Kosik
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-20Fix bug #4825: [clear] should not dependency-check hypotheses that come above...Pierre-Marie Pédrot
2016-06-18Reuse the typing_flags datatype for inductives.Pierre-Marie Pédrot
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:30:06 +0000