index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
fixed bug #2375 (congruence)
corbinea
2010-09-02
*
* removed declare_constant and declare_internal_constant
vsiles
2010-09-02
*
v13392 port from v8.3 to trunk : correct message when defining inductive schemes
vsiles
2010-09-02
*
Clarified role of Set Boolean Equality Schemes wrt Set Equality Scheme +
herbelin
2010-09-02
*
Improved printing of Unfoldable constants in hints databases (used
herbelin
2010-09-02
*
* By default, load proof terms.
regisgia
2010-08-31
*
* scripts/Coqc toplevel/Usage:
regisgia
2010-08-27
*
* checker/Safe_typing.LightenLibrary:
regisgia
2010-08-27
*
* kernel/Safe_typing.LightenLibrary:
regisgia
2010-08-27
*
* (checker|kernel)/Safe_typing:
regisgia
2010-08-27
*
* (checker|kernel)/Safe_typing:
regisgia
2010-08-27
*
* toplevel/Coqtop: Reactivate -dont-load-proofs option.
regisgia
2010-08-27
*
* library/Library: Reformulate a comment.
regisgia
2010-08-27
*
* library/Library: Document.
regisgia
2010-08-27
*
* checker/SafeTyping kernel/SafeTyping:
regisgia
2010-08-27
*
* lib/Flags: Replace dont_load_proofs by load_proofs since not loading
regisgia
2010-08-27
*
* Improve documentation of LightenLibrary.
regisgia
2010-08-27
*
* (checker|kernel)/Safe_typing: New LightenLibrary.
regisgia
2010-08-27
*
* library/Library: Remove the use of the old-fashioned lighten_library.
regisgia
2010-08-27
*
* library/Library: Remove lighten_library definition.
regisgia
2010-08-27
*
Fix an error message ot having the ERror: prefix.
courtieu
2010-08-26
*
Export printing functions for extra arguments. Maybe there's a way to
msozeau
2010-08-03
*
Fix [clenv_missing] to compute a better approximation of missing
msozeau
2010-08-02
*
Fixed commit r13359 which was incomplete for its "trunk" part. Thanks
herbelin
2010-07-31
*
adpated the checker to handle coomutative cuts and lazyness
barras
2010-07-30
*
Removed information in COMPATIBILITY that were intended before all for
herbelin
2010-07-30
*
better fix to bug #2319: types are compiled in the env of the bodies
barras
2010-07-30
*
Updated test on Nsatz after Loïc moved NsatzR to Nsatz.
herbelin
2010-07-30
*
Capitulation wrt "change pat with term": instead of solving the
herbelin
2010-07-30
*
r13359 continued: removed native treatment for λ (lambda) and Π (Pi)
herbelin
2010-07-30
*
Rather quick hack to make basic unicode notations available by
herbelin
2010-07-29
*
Fixed a bug introduced (r13316/r13329) in the printing of notations
herbelin
2010-07-29
*
kernel conversion and reduction do not raise assert failure on ill-typed term...
barras
2010-07-29
*
test-case for bug #2105
barras
2010-07-29
*
fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...
barras
2010-07-29
*
fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...
barras
2010-07-29
*
Fix bug #2209, don't use the fragile argument name "y" to pass the
msozeau
2010-07-28
*
Rewrite Heap merging so that it extracts to an O(n log n) definition.
msozeau
2010-07-28
*
unification des tactiques nsatz pour R Z avec celle des anneaux integres
pottier
2010-07-28
*
oops. commited files I shouldn't have. reverting on r13341
barras
2010-07-28
*
ported r13340 to trunk
barras
2010-07-28
*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0...
pottier
2010-07-28
*
fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodies
barras
2010-07-28
*
nstaz pour les anneaux integres et les setoides, R Z et Q
pottier
2010-07-27
*
Fix computation of fix annotation index: only consider assumptions and
msozeau
2010-07-27
*
Minor fixes:
msozeau
2010-07-27
*
Documentation of Set Automatic Coercions Import.
herbelin
2010-07-25
*
Fix installation of emacs files
glondu
2010-07-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Updated COPYRIGHT file and header. Improved and fixed header updater.
herbelin
2010-07-24
[next]