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
*
Extraction Library Foo creates Foo.ml, not foo.ml
letouzey
2010-07-07
*
CHANGES: mention last-minute improvements of extraction
letouzey
2010-07-07
*
Extraction: get advantage of nicer, algebraic, module types
letouzey
2010-07-07
*
Extraction: some more work on the (re)naming framework
letouzey
2010-07-07
*
Mod_typing: fix the content of the typ_expr_alg field
letouzey
2010-07-07
*
Fix goal display when backtracking
vgross
2010-07-05
*
Robustness fix : clean restart of coqtop on pipe error + force matching
vgross
2010-07-05
*
Turned off Mac dynlink hack for 10.6.3+ on x86_64
thutchin
2010-07-05
*
Stronger checks on coqtop termination, warning when zombies.
vgross
2010-07-05
*
Extraction: (yet another) rework of the renaming code
letouzey
2010-07-05
*
FSets/Msets: some renaming of module params to simplify the task of the extra...
letouzey
2010-07-05
*
Fixing tabs closing problems by removing activation infrastructure.
vgross
2010-07-02
*
Extraction: better support of modules
letouzey
2010-07-02
*
Extraction: no more MPself hence no need for subst during pp
letouzey
2010-07-02
*
Remove dependency to Unix from module Profile
glondu
2010-07-02
*
Sorting library: export as hints only lemmas that obviously simplify
herbelin
2010-07-02
*
Miscellaneous small updates:
herbelin
2010-07-01
*
Move [delayed] to util and use [force_delayed] everywhere to force
msozeau
2010-06-30
*
Fix generalize_eqs tactic to not consider defined variables as being generali...
msozeau
2010-06-30
*
Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.
msozeau
2010-06-30
*
Correct wrong handling of evars in instance definitions that prevented
msozeau
2010-06-29
*
QArith: typo in name of hint db (fix #2346)
letouzey
2010-06-29
*
change the flag "internal" in declare/ind_tables from bool to
vsiles
2010-06-29
*
Made tclABSTRACT normalize evars before saying it does not support
herbelin
2010-06-29
*
Fix compilation by replacing some "auto with zarith" with "ring"
glondu
2010-06-28
*
Extraction: handling modules (not functors) in Haskell by name mangling
letouzey
2010-06-28
*
Update of documentation for the standard library (cf. #2332)
letouzey
2010-06-28
*
Extraction: remove a useless match
letouzey
2010-06-28
*
Made "replace" accepts open terms on its left-hand-side.
herbelin
2010-06-28
*
Fixed a bug introduced in a combination in r12807 and revealed in
herbelin
2010-06-28
*
Applying François' patches about Canonical Projections (see #2302 and #2334).
herbelin
2010-06-26
*
Backporting modifications to nsatz (doc + fix of bug #2328) from trunk to v8.3.
herbelin
2010-06-26
*
Moved error when option does not exist into a warning (this allows to
herbelin
2010-06-25
*
bug 2328 fixed: failure when polynomial not i ideal
pottier
2010-06-25
*
modifs de nsatz suggerees par Hugo
pottier
2010-06-25
*
Restored a "feature" of unification in pre-8.3 (it was used e.g. in a
herbelin
2010-06-25
*
Extraction: nicer simple extraction of custom defs (fix #2204)
letouzey
2010-06-23
*
Names: remove obsolete mod_self_id
letouzey
2010-06-23
*
Ajout d'une feuille de style pour les définitions spécifiques à Hevea + di...
notin
2010-06-23
*
Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ...
notin
2010-06-23
*
Commit 13179 continued (updated CHANGES about support for Heq's library).
herbelin
2010-06-22
*
Backport from trunk to 8.3 of modifications on groebner/nsatz
herbelin
2010-06-22
*
Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).
herbelin
2010-06-22
*
Fixing dependencies for coqide
vgross
2010-06-22
*
fix bug #2318, parsing error on dos line endings
vgross
2010-06-22
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Protection against anomaly when loading a state with bad magic number.
herbelin
2010-06-22
*
Extraction: replace unicode characters in ident by ascii encodings (fix #2158...
letouzey
2010-06-21
*
Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)
letouzey
2010-06-20
*
clear/revert dependent: restrict to hyp(h) instead of ident(h)
letouzey
2010-06-18
[next]