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
*
New version of 12650 that was broken (supporting again records when
herbelin
2010-01-12
*
revert commit 12650 for the moment, since it breaks MSetAVL
letouzey
2010-01-12
*
Temporary fix to compensate the loss of descent on dependent
herbelin
2010-01-12
*
Errors issued by reduction tactics (e.g. pattern) were not caught by "try".
herbelin
2010-01-04
*
Regression test for bug #2145 (Groebner failing with "not eq" hypotheses).
herbelin
2009-12-30
*
Fixing bug #2193: computation of dependencies in the "match" return
herbelin
2009-12-30
*
Fixing bug #2146 (broken selection of occurrences in "change").
herbelin
2009-12-30
*
Renouncing to have the option "Automatic Introduction" on by default.
herbelin
2009-12-29
*
Improving descend_in_conjunctions (using a combinators instead of a tactic)
herbelin
2009-12-29
*
In "simpl c" and "change c with d", c can be a pattern.
herbelin
2009-12-24
*
Made the side-conditions of lemmas always come last when chaining "apply in"
herbelin
2009-12-13
*
Revision 12557 continued (better rendering of dependent rewrite)
herbelin
2009-12-13
*
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
[next]