aboutsummaryrefslogtreecommitdiff
path: root/kernel/environ.ml
AgeCommit message (Expand)Author
2016-10-12Remove dead code in Environ.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-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
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-24Make the retroknowledge marshalable.Arnaud Spiwack
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-13Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).Hugo Herbelin
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06- Rename eq to equal in Univ, document new modules, set interfaces.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-04-09Int31 decompilation in native compiler was still partial. Now fixed.Maxime Dénès
2014-04-09Machine arithmetic operations for native compiler.Maxime Dénès
2014-04-09Full support for int31 values in native compiler.Maxime Dénès
2014-04-09Partial support for open terms in int31.Maxime Dénès
2014-03-14Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:42:45 +0000