aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.mli
Commit message (Expand)AuthorAge
* Moving the typing_flags to the environment.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
* | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* | 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
* Update headers.Gravatar Maxime Dénès2015-01-12
* selective join/export of the safe_environmentGravatar Enrico Tassi2014-10-13
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* - 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
* 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
* .vi files: .vo files without proofsGravatar Enrico Tassi2014-01-04
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
* ind_tables: properly handling side effectsGravatar gareuselesinge2013-08-30
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Safe_typing code refactoringGravatar letouzey2013-08-20
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* 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
* Minor simplifications in Declaremods and Safe_typingGravatar letouzey2013-04-15
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* 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
* Updating headers.Gravatar herbelin2012-08-08
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
* Rely on kernel to know if a name is already used so as to be consistent with it.Gravatar herbelin2011-10-08
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* * Improve documentation of LightenLibrary.Gravatar regisgia2010-08-27
* * (checker|kernel)/Safe_typing: New LightenLibrary.Gravatar regisgia2010-08-27
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
* Include Self (Type) Foo: applying a (Type) Functor to the current contextGravatar letouzey2009-11-16