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
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Universes algorithm : clarified comments
Jacques-Henri Jourdan
2016-01-17
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-13
|
\
|
*
|
merge
Matej Kosik
2016-01-11
|
\
\
|
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
|
COMMENTS: of "Constr.case_info" type were updated.
Matej Kosik
2016-01-11
*
|
|
COMMENTS: added to the "Names.inductive" and "Names.constructor" types.
Matej Kosik
2016-01-11
|
|
*
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
*
|
|
Merge remote-tracking branch 'origin/v8.5' into trunk
Guillaume Melquiond
2016-01-06
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Protect code against changes in Map interface.
Maxime Dénès
2016-01-06
*
|
|
Merge remote-tracking branch 'origin/v8.5' into trunk
Guillaume Melquiond
2016-01-05
|
\
|
|
|
*
|
Fix handling of side-effects in case of `Opaque side-effects as well.
Matthieu Sozeau
2016-01-04
*
|
|
Remove some unused functions.
Guillaume Melquiond
2016-01-02
*
|
|
Avoid warnings about loop indices.
Guillaume Melquiond
2016-01-02
*
|
|
Fix typos.
Guillaume Melquiond
2016-01-01
*
|
|
Remove unused open.
Guillaume Melquiond
2016-01-01
|
*
|
Fix bug #4456, anomaly in handle-side effects
Matthieu Sozeau
2015-12-31
*
|
|
Merge branch 'v8.5' into trunk
Guillaume Melquiond
2015-12-31
|
\
|
|
*
|
|
Removing dead code.
Pierre-Marie Pédrot
2015-12-27
|
|
*
COMMENTS: of "Constr.case_info" type were updated.
Matej Kosik
2015-12-22
|
|
*
COMMENTS: added to the "Names.inductive" and "Names.constructor" types.
Matej Kosik
2015-12-22
|
|
/
|
/
|
|
*
Inclusion of functors with restricted signature is now forbidden (fix #3746)
Pierre Letouzey
2015-12-22
*
|
COMMENTS: added to the "Constr.case_info" type.
Matej Kosik
2015-12-18
*
|
COMMENTS: added to some variants of the "Constr.kind_of_term" type.
Matej Kosik
2015-12-18
*
|
COMMENTS: added to the "Names" module.
Matej Kosik
2015-12-18
*
|
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
[next]