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
...
*
|
ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_conv
Matej Kosik
2015-12-17
*
|
ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_conv
Matej Kosik
2015-12-17
*
|
CLEANUP: in the Reduction module
Matej Kosik
2015-12-17
*
|
CLEANUP: in the Reduction module
Matej Kosik
2015-12-17
*
|
Fixing e3cefca41b about supposingly simplifying primitive projections
Hugo Herbelin
2015-12-15
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-11
|
\
|
|
*
bug fixes to vm computation + test cases.
Gregory Malecha
2015-12-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
|
|
*
Fix some typos.
Guillaume Melquiond
2015-12-07
*
|
Unifying betazeta_applist and prod_applist into a clearer interface.
Hugo Herbelin
2015-12-05
*
|
Slight simplification of the code of primitive projection (in relation
Hugo Herbelin
2015-12-05
*
|
Moving extended_rel_vect/extended_rel_list to the kernel.
Hugo Herbelin
2015-12-05
*
|
About building of substitutions from instances.
Hugo Herbelin
2015-12-05
*
|
Experimenting documentation of the Vars.subst functions.
Hugo Herbelin
2015-12-05
*
|
Contracting one extra beta-redex on the fly when typing branches of "match".
Hugo Herbelin
2015-12-05
*
|
A few renaming and simplification in inductive.ml.
Hugo Herbelin
2015-12-05
*
|
Moving three related small half-general half-ad-hoc utility functions
Hugo Herbelin
2015-12-05
*
|
New algorithm for universe cycle detections.
Jacques-Henri Jourdan
2015-12-01
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
|
*
Univs: entirely disallow instantiation of polymorphic constants with
Matthieu Sozeau
2015-11-27
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-26
|
\
|
|
*
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
|
\
|
|
*
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
*
|
Hashconsing modules.
Pierre-Marie Pédrot
2015-11-15
*
|
Merge origin/v8.5 into trunk
Hugo Herbelin
2015-11-10
|
\
|
|
*
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
*
Univs: update refman, better printers for universe contexts.
Matthieu Sozeau
2015-11-04
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-30
|
\
|
|
*
Collect subproof universes in handle_side_effects.
Matthieu Sozeau
2015-10-29
|
*
Cleanup API and comments of 908dcd613
Enrico Tassi
2015-10-29
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-26
|
\
|
|
*
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-19
|
\
|
|
*
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
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-10-16
|
\
|
[prev]
[next]