index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
Commit message (
Expand
)
Author
Age
*
A patch renaming equal into eq in the module dealing with
Hugo Herbelin
2016-03-22
*
Adding eq/compare/hash for syntactic view at
Hugo Herbelin
2016-03-22
*
Primitive projections: protect kernel from erroneous definitions.
Matthieu Sozeau
2016-03-10
*
Hashconsing modules.
Pierre-Marie Pédrot
2016-03-10
*
This fix is probably not enough to justify that there are no problems with
Maxime Dénès
2016-03-04
*
Rename Ephemeron -> CEphemeron.
Maxime Dénès
2016-03-04
*
Fixing bde12b70 about reporting ill-formed constructor.
Hugo Herbelin
2016-01-26
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Be more verbose about failure to compile libraries to native code.
Guillaume Melquiond
2016-01-08
*
Fix a misleading comment for substn_vars
Matthieu Sozeau
2016-01-07
*
Protect code against changes in Map interface.
Maxime Dénès
2016-01-06
*
Fix handling of side-effects in case of `Opaque side-effects as well.
Matthieu Sozeau
2016-01-04
*
Fix bug #4456, anomaly in handle-side effects
Matthieu Sozeau
2015-12-31
*
Inclusion of functors with restricted signature is now forbidden (fix #3746)
Pierre Letouzey
2015-12-22
*
bug fixes to vm computation + test cases.
Gregory Malecha
2015-12-09
*
Fix some typos.
Guillaume Melquiond
2015-12-07
*
Univs: entirely disallow instantiation of polymorphic constants with
Matthieu Sozeau
2015-11-27
*
Fix output of universe arcs. (Fix bug #4422)
Guillaume Melquiond
2015-11-23
*
Fixing kernel bug in typing match with let-ins in the arity.
Hugo Herbelin
2015-11-22
*
Fixing fix c71aa6b to primitive projections.
Hugo Herbelin
2015-11-18
*
Slightly documenting code for building primitive projections.
Hugo Herbelin
2015-11-18
*
Fixing logical bugs in the presence of let-ins in computiong primitive
Hugo Herbelin
2015-11-18
*
Dead code from the commit having introduced primitive projections (a4043608).
Hugo Herbelin
2015-11-10
*
Fixing a bug in reporting ill-formed constructor.
Hugo Herbelin
2015-11-10
*
Univs: update refman, better printers for universe contexts.
Matthieu Sozeau
2015-11-04
*
Collect subproof universes in handle_side_effects.
Matthieu Sozeau
2015-10-29
*
Cleanup API and comments of 908dcd613
Enrico Tassi
2015-10-29
*
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-10-28
*
Refine Gregory Malecha's patch on VM and universe polymorphism.
Maxime Dénès
2015-10-28
*
Conversion of polymorphic inductive types was incomplete in VM and native.
Maxime Dénès
2015-10-28
*
Fix minor typo in native compiler.
Maxime Dénès
2015-10-28
*
Adds support for the virtual machine to perform reduction of universe polymor...
Gregory Malecha
2015-10-28
*
Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)
Pierre Letouzey
2015-10-25
*
Minor module cleanup : error HigherOrderInclude was never happening
Pierre Letouzey
2015-10-25
*
Fixing a bug in reporting ill-formed inductive.
Hugo Herbelin
2015-10-22
*
Miscellaneous typos, spacing, US spelling in comments or variable names.
Hugo Herbelin
2015-10-18
*
Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,
Hugo Herbelin
2015-10-18
*
Remove left2right reference from the kernel.
Maxime Dénès
2015-10-16
*
Avoid dependency of the pretyper on C code.
Maxime Dénès
2015-10-15
*
Fix #4346 2/2: VM casts were not inferring universe constraints.
Maxime Dénès
2015-10-15
*
Fix #4346 1/2: native casts were not inferring universe constraints.
Maxime Dénès
2015-10-15
*
Warn user when bytecode compilation fails.
Maxime Dénès
2015-10-15
*
Remove now useless exception handler in default conversion.
Maxime Dénès
2015-10-15
*
Fix detection of ties in oracle_order.
Guillaume Melquiond
2015-10-15
*
Univs: inductives, remove unneeded test
Matthieu Sozeau
2015-10-14
*
Temporary fix: kernel conversion needs to ignore l2r flag.
Maxime Dénès
2015-10-14
*
Remove reference to default conversion function inside the kernel.
Maxime Dénès
2015-10-14
*
Remove -vm flag of coqtop.
Maxime Dénès
2015-10-14
*
Remove unused infos structure in VM.
Maxime Dénès
2015-10-14
*
Make interpreter of PROJ simpler by not using the stack.
Guillaume Melquiond
2015-10-14
[next]