aboutsummaryrefslogtreecommitdiff
path: root/kernel/environ.mli
AgeCommit message (Expand)Author
2016-10-12Remove dead code in Environ.Pierre-Marie Pédrot
2016-09-09Removing the now useless field env_named_val from named_context_val.Pierre-Marie Pédrot
2016-09-09Packing the named_context_val in a proper record and marking it private.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-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-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-10-02Forcing i > Set for global universes (incomplete)Matthieu Sozeau
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-12Update headers.Maxime Dénès
2014-11-12Cleaner interfaces for linking locations of native compiler.Maxime Dénès
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-09-24Make the retroknowledge marshalable.Arnaud Spiwack
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-06-13Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).Hugo Herbelin
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.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-01-05Environ: export API to transitively close a set of section variablesEnrico Tassi
2013-12-28Removing native_name reference from constant_body.Maxime Dénès
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
2013-10-22Removing some generic equalities.ppedrot
2013-08-25Replacing lists by sets in clear tactic.ppedrot
2013-08-20Safe_typing code refactoringletouzey
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2011-10-26Environ.set_universes is dead codeletouzey
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ...letouzey
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-12-01Continuing r12485-12486 (cleaning around name generation)herbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 21:04:32 +0000