aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/global.mli
Commit message (Expand)AuthorAge
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* Adding a local type-in-type flag in kernel declarations.Gravatar Pierre-Marie Pédrot2016-06-18
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\| |
| * | Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* | | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
|/ /
* | Univs: Change intf of push_named_def to return the computed universeGravatar Matthieu Sozeau2015-10-02
* | Univs: refined handling of assumptionsGravatar Matthieu Sozeau2015-10-02
| * Propagate `Guarded` flag from syntax to kernel.Gravatar Arnaud Spiwack2015-09-25
* | Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
* | Native compiler: refactor code handling pre-computed values.Gravatar Maxime Dénès2015-07-10
|/
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Better comment for [type_of_global_unsafe].Gravatar Matthieu Sozeau2015-02-16
* Comment on the unsafe_ functions in Global.Gravatar Matthieu Sozeau2015-02-16
* Update headers.Gravatar Maxime Dénès2015-01-12
* Global: export the name of the summary entryGravatar Enrico Tassi2014-12-17
* selective join/export of the safe_environmentGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Safe_typing code refactoringGravatar letouzey2013-08-20
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Added a Register Inline command for the native compiler. Will be ported to th...Gravatar mdenes2013-07-10
* Use definition_entry to declare local definitionsGravatar gareuselesinge2013-05-09
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Minor simplifications in Declaremods and Safe_typingGravatar letouzey2013-04-15
* Dir_path --> DirPathGravatar letouzey2013-02-19
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
* Various simplifications about constant_of_delta and mind_of_deltaGravatar letouzey2011-10-11
* Rely on kernel to know if a name is already used so as to be consistent with it.Gravatar herbelin2011-10-08