aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.mli
Commit message (Expand)AuthorAge
* Let definitions do not create new universe constraints.Gravatar Pierre-Marie Pédrot2017-12-19
* Specific type for section definition entries.Gravatar Pierre-Marie Pédrot2017-12-19
* Let definitions must not contain side-effects when reaching the kernel.Gravatar Pierre-Marie Pédrot2017-12-16
* [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [stm] [flags] Move document mode flags to the STM.Gravatar Emilio Jesus Gallego Arias2017-10-06
* Statically ensuring that inlined entries out of the kernel have no effects.Gravatar Pierre-Marie Pédrot2017-07-26
* Further simplication: do not recreate entries for side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
* Remove a horrendous hack in Declare to retrieve exported side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
* More precise type of entries capturing their lack of side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Documenting the API of side-effects.Gravatar Pierre-Marie Pédrot2017-03-23
* Making the side_effects type opaque.Gravatar Pierre-Marie Pédrot2017-03-23
* 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