aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* congruence: Restrict refreshing to SetGravatar Matthieu Sozeau2016-07-04
* Fix potential race condition in vm_compute.Gravatar Guillaume Melquiond2016-05-31
* native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* Fixing an incompatility introduced in a404360: kernel conversion wasGravatar Hugo Herbelin2016-04-27
* A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2016-03-22
* Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2016-03-22
* Primitive projections: protect kernel from erroneous definitions.Gravatar Matthieu Sozeau2016-03-10
* Hashconsing modules.Gravatar Pierre-Marie Pédrot2016-03-10
* This fix is probably not enough to justify that there are no problems withGravatar Maxime Dénès2016-03-04
* Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* Fixing bde12b70 about reporting ill-formed constructor.Gravatar Hugo Herbelin2016-01-26
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Be more verbose about failure to compile libraries to native code.Gravatar Guillaume Melquiond2016-01-08
* Fix a misleading comment for substn_varsGravatar Matthieu Sozeau2016-01-07
* Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
* Fix handling of side-effects in case of `Opaque side-effects as well.Gravatar Matthieu Sozeau2016-01-04
* Fix bug #4456, anomaly in handle-side effectsGravatar Matthieu Sozeau2015-12-31
* Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
* bug fixes to vm computation + test cases.Gravatar Gregory Malecha2015-12-09
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* Fix output of universe arcs. (Fix bug #4422)Gravatar Guillaume Melquiond2015-11-23
* Fixing kernel bug in typing match with let-ins in the arity.Gravatar Hugo Herbelin2015-11-22
* Fixing fix c71aa6b to primitive projections.Gravatar Hugo Herbelin2015-11-18
* Slightly documenting code for building primitive projections.Gravatar Hugo Herbelin2015-11-18
* Fixing logical bugs in the presence of let-ins in computiong primitiveGravatar Hugo Herbelin2015-11-18
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 16:54:14 +0000