index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
Commit message (
Expand
)
Author
Age
*
Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)
herbelin
2009-12-03
*
Continuing r12485-12486 and r12549 (cleaning around name generation)
herbelin
2009-12-02
*
Remove interface plugin
glondu
2009-12-02
*
Continuing r12485-12486 (cleaning around name generation)
herbelin
2009-12-01
*
Fix backtracking heuristic in typeclass resolution.
msozeau
2009-11-30
*
Added support for definition of fixpoints using tactics.
herbelin
2009-11-27
*
Substitute terms for evars-as-goals as soon as they are solved in
msozeau
2009-11-27
*
Fixing xml theory file export (was not consistent with coqdoc file
herbelin
2009-11-26
*
Fix test-suite scripts: [Generalizable Variables] and small
msozeau
2009-11-13
*
Restore test-suite/csdp.cache erased from svn by mistake
letouzey
2009-11-12
*
BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)
letouzey
2009-11-12
*
Repair interpretation of numeral for BigQ, add a printer (close #2160)
letouzey
2009-11-12
*
Redoing broken commit r12498 (fixing bug #2167 + attempt to test the
herbelin
2009-11-11
*
Fixing bug #2167 + attempt to test the compatibility of a more robust
herbelin
2009-11-11
*
Test for bug #2168, forgotten in r12496.
herbelin
2009-11-11
*
Fixed bug #2168 (closing a section may have as side-effect the erasure
herbelin
2009-11-11
*
Improving abbreviations/notations + backtrack of semantic change in r12439
herbelin
2009-11-11
*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12483 85f007b7-540e-0...
fbesson
2009-11-09
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Attempt to capture on time unification errors for "with" bindings.
herbelin
2009-10-30
*
Revision 12439 continued, printing part (notations to names behave
herbelin
2009-10-29
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
Made that notations to names behave like the names they refer to wrt
herbelin
2009-10-28
*
Local/Global revision 12418 continued
herbelin
2009-10-26
*
Adapted test unfold.v after eq gets its argument maximally inserted
herbelin
2009-10-26
*
Restore (and test) broken chaining of lemmas in "apply in" in presence
herbelin
2009-10-25
*
Add support for remaining side-conditions in "apply in as".
herbelin
2009-10-25
*
Improved the treatment of Local/Global options (noneffective Local on
herbelin
2009-10-25
*
Fixed a notation bug when extending binder_constr with empty levels
herbelin
2009-10-17
*
Fixed a bug introduced in revision 12265.
herbelin
2009-10-08
*
Removal of trailing spaces.
serpyc
2009-10-04
*
Fixed a bug in the interaction between dEqThen and inject_at_positions
herbelin
2009-09-27
*
Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.
herbelin
2009-09-27
*
Delay the choice of eliminator in destruct/induction until we know if
herbelin
2009-09-27
*
Micromega doc : psatz Z -> psatz Z 2
fbesson
2009-09-24
*
Add the option to automatically introduce variables declared before the
msozeau
2009-09-22
*
Only one "in" clause in "destruct" even for a multiple "destruct".
herbelin
2009-09-20
*
micromega: better handling of exponentiation + correction of test-suite termi...
fbesson
2009-09-18
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0...
fbesson
2009-08-25
*
+ csdp.cache
fbesson
2009-08-15
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
Ensures that let-in's in arities of inductive types work well. Maybe not
herbelin
2009-08-11
*
Relatively ad hoc fix to an ill-typed instantiation bug in type
herbelin
2009-08-11
*
psatz Z -> psatz Z 1
fbesson
2009-07-30
*
Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"
letouzey
2009-07-24
*
Move some examples for groebner into a test-suite file
letouzey
2009-07-20
*
- Granted wish #2138 (support for local binders in syntax of Record fields).
herbelin
2009-07-15
*
Reactivation of pattern unification of evars in apply unification, in
herbelin
2009-07-08
*
Fixing bug #2106 ("match" compilation with multi-dependent constructor).
herbelin
2009-06-06
[next]