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
*
Remove kind_of_type, kind_of_term2 (dead code)
glondu
2010-09-28
*
Partial review of removed dead code (r13460)
herbelin
2010-09-24
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Fix inconsistency in Prop/Set conversion check
glondu
2010-09-23
*
Added eta-expansion in kernel, type inference and tactic unification,
herbelin
2010-09-20
*
Sharing is not anymore broken by traverse_module.
soubiran
2010-09-15
*
Fix likely semantic typos
glondu
2010-09-15
*
* kernel/Safe_typing.LightenLibrary:
regisgia
2010-08-27
*
* (checker|kernel)/Safe_typing:
regisgia
2010-08-27
*
* (checker|kernel)/Safe_typing:
regisgia
2010-08-27
*
* checker/SafeTyping kernel/SafeTyping:
regisgia
2010-08-27
*
* Improve documentation of LightenLibrary.
regisgia
2010-08-27
*
* (checker|kernel)/Safe_typing: New LightenLibrary.
regisgia
2010-08-27
*
better fix to bug #2319: types are compiled in the env of the bodies
barras
2010-07-30
*
kernel conversion and reduction do not raise assert failure on ill-typed term...
barras
2010-07-29
*
fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...
barras
2010-07-29
*
ported r13340 to trunk
barras
2010-07-28
*
fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodies
barras
2010-07-28
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
fixed (serious) bug #2353: non-recursive parameters of nested inductive types...
barras
2010-07-16
*
removed a potentially dangerous try ... with _ -> ...
barras
2010-07-16
*
Mod_typing: fix the content of the typ_expr_alg field
letouzey
2010-07-07
*
Names: remove obsolete mod_self_id
letouzey
2010-06-23
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Added printing of recursive notations in cases pattern (supported by wish 2248).
herbelin
2010-06-14
*
Fixing spelling: pr_coma -> pr_comma
herbelin
2010-06-12
*
"Improved" the form of the inferred type of "match" by
herbelin
2010-06-03
*
fixed guard check with commutative cuts
barras
2010-05-20
*
Mrec was not substituted correctly
barras
2010-05-20
*
Discontinue support for ocaml 3.09.*
letouzey
2010-05-19
*
Some ocamldoc comments + Fixing name of .coqrc.version file in refman
pboutill
2010-05-18
*
Applicative commutative cuts in Fixpoint guard condition
pboutill
2010-05-18
*
Removed $Id$ introduced inadvertently in r13005 (no more $Id$ since r12972)
herbelin
2010-05-09
*
Added a few informations about file lineages (for the most part in kernel)
herbelin
2010-05-09
*
"make source-doc" builds documentation of mli in html and pdf at
pboutill
2010-04-29
*
After the approval of Bruno, here the patch for the checker.
soubiran
2010-04-29
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
fixed bug #2224 (Error message in positivity check fixed)
vsiles
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)
herbelin
2010-04-20
*
In function "substitution_prefixed_by" the prefix test on module path
soubiran
2010-04-19
*
cf. 12945
soubiran
2010-04-16
*
Names.mli: double declaration of mind_modpath
letouzey
2010-04-16
*
fixed confusion between number of cstr arguments and number of pattern variab...
barras
2010-03-12
*
introduced lazy computation of size info in the guard condition
barras
2010-03-11
*
Added a lazy evaluation of the composition of module substitutions. It improv...
soubiran
2010-02-04
*
fix commit 12706 + comments.
soubiran
2010-02-03
*
Small fix on module inclusion.
soubiran
2010-02-02
[next]