aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Dead code from the commit having introduced primitive projections (a4043608).Gravatar Hugo Herbelin2015-11-10
* Fixing a bug in reporting ill-formed constructor.Gravatar Hugo Herbelin2015-11-10
* Univs: update refman, better printers for universe contexts.Gravatar Matthieu Sozeau2015-11-04
* Collect subproof universes in handle_side_effects.Gravatar Matthieu Sozeau2015-10-29
* Cleanup API and comments of 908dcd613Gravatar Enrico Tassi2015-10-29
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Refine Gregory Malecha's patch on VM and universe polymorphism.Gravatar Maxime Dénès2015-10-28
* Conversion of polymorphic inductive types was incomplete in VM and native.Gravatar Maxime Dénès2015-10-28
* Fix minor typo in native compiler.Gravatar Maxime Dénès2015-10-28
* Adds support for the virtual machine to perform reduction of universe polymor...Gravatar Gregory Malecha2015-10-28
* Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)Gravatar Pierre Letouzey2015-10-25
* Minor module cleanup : error HigherOrderInclude was never happeningGravatar Pierre Letouzey2015-10-25
* Fixing a bug in reporting ill-formed inductive.Gravatar Hugo Herbelin2015-10-22
* Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
* Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,Gravatar Hugo Herbelin2015-10-18
* Remove left2right reference from the kernel.Gravatar Maxime Dénès2015-10-16
* Avoid dependency of the pretyper on C code.Gravatar Maxime Dénès2015-10-15
* Fix #4346 2/2: VM casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* Fix #4346 1/2: native casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* Warn user when bytecode compilation fails.Gravatar Maxime Dénès2015-10-15
* Remove now useless exception handler in default conversion.Gravatar Maxime Dénès2015-10-15
* Fix detection of ties in oracle_order.Gravatar Guillaume Melquiond2015-10-15
* Univs: inductives, remove unneeded testGravatar Matthieu Sozeau2015-10-14
* Temporary fix: kernel conversion needs to ignore l2r flag.Gravatar Maxime Dénès2015-10-14
* Remove reference to default conversion function inside the kernel.Gravatar Maxime Dénès2015-10-14
* Remove -vm flag of coqtop.Gravatar Maxime Dénès2015-10-14
* Remove unused infos structure in VM.Gravatar Maxime Dénès2015-10-14
* Make interpreter of PROJ simpler by not using the stack.Gravatar Guillaume Melquiond2015-10-14
* Remove some unused variables.Gravatar Guillaume Melquiond2015-10-14
* Fix some typos.Gravatar Guillaume Melquiond2015-10-14
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Univs: be more restrictive for template polymorphic constants: onlyGravatar Matthieu Sozeau2015-10-12
* Gather VM tags in Cbytecodes.Gravatar Maxime Dénès2015-10-12
* Complete handling of primitive projections in VM.Gravatar Maxime Dénès2015-10-09
* Code cleaning in VM (with Benjamin).Gravatar Maxime Dénès2015-10-09
* Univs: fix bug #3807Gravatar Matthieu Sozeau2015-10-08
* Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* term_typing: strengthen discharging codeGravatar Enrico Tassi2015-10-08
* Univs: fix bug #4288, Print Sorted generated backward < constraints.Gravatar Matthieu Sozeau2015-10-05
* 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
* Univs: forgot a substitution in mod_typing.Gravatar Matthieu Sozeau2015-10-02
* Univs: correct handling of with in modulesGravatar Matthieu Sozeau2015-10-02
* Univs: fix bug #4251, handling of template polymorphic constants.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix subtyping of polymorphic parameters.Gravatar Matthieu Sozeau2015-10-02
* Univs: uncovered bug in strengthening of opaque polymorphic definitions.Gravatar Matthieu Sozeau2015-10-02
* Univs: handle side-effects of futures correctly in kernel.Gravatar Matthieu Sozeau2015-10-02
* Univs (kernel) adapt to new invariantsGravatar Matthieu Sozeau2015-10-02
* Univs: module constraints move to universe contexts as they mightGravatar Matthieu Sozeau2015-10-02
* Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 01:05:52 +0000