aboutsummaryrefslogtreecommitdiff
path: root/kernel/environ.ml
AgeCommit message (Expand)Author
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
2016-06-18Adding a local type-in-type flag in kernel declarations.Pierre-Marie Pédrot
2016-02-15CLEANUP: Simplifying the changes done in "kernel/*"Matej Kosik
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
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Univs: module constraints move to universe contexts as they mightMatthieu Sozeau
2015-10-02Forcing i > Set for global universes (incomplete)Matthieu Sozeau
2015-09-10Assertion checking that invariant enforced by 0f8d1b92 always holds.Maxime Dénès
2015-08-02Fixing pop_rel_context.Hugo Herbelin
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Fixing pop_rel_contextHugo Herbelin
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-03-25Fix vm compiler to refuse to compile code making use of inductives withMatthieu Sozeau
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2014-11-12Cleaner interfaces for linking locations of native compiler.Maxime Dénès
2014-10-24Fix retroknowledge for int31 division.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:29:14 +0000