index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
bugs
Commit message (
Expand
)
Author
Age
...
*
Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).
herbelin
2010-07-21
*
Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.
msozeau
2010-06-30
*
Backporting modifications to nsatz (doc + fix of bug #2328) from trunk to v8.3.
herbelin
2010-06-26
*
Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)
letouzey
2010-06-20
*
add in test-suite the scripts about fsetdec bugs
letouzey
2010-06-18
*
test for bug #2141 (include + extraction)
letouzey
2010-06-16
*
Fixing bug 2295 (omission of option "as" in return clause of "match" was not
herbelin
2010-06-13
*
Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).
herbelin
2010-06-13
*
Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem with
herbelin
2010-06-13
*
Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"
herbelin
2010-06-13
*
Fixed bug #2135 (second-order unification was raising cryptic message)
herbelin
2010-06-12
*
Added regression tests for bugs + miscellaneous improvements
herbelin
2010-06-12
*
Fixed bug # 2303 in r 13087.
msozeau
2010-06-09
*
Fix bug #2262: bad implicit argument number by avoiding counting
msozeau
2010-06-09
*
Automatic introduction of names given before ":" in Lemma's and
herbelin
2010-06-09
*
Fix bug 2307
pboutill
2010-05-20
*
Backporting r13007 (evar_merge wrong and costly) to V8.3 and added test.
herbelin
2010-05-10
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)
herbelin
2010-04-20
*
Propagated fix to bug 2127 (Hint Rewrite badly globalized in modules) to 8.2
herbelin
2010-04-20
*
Test for bug #2231 (unexpected error when using let/if over an inductive
herbelin
2010-04-10
*
Granting wish #2251 thanks to commit 12900 solved bug 1416.v (which
herbelin
2010-04-07
*
Granting wish #2251 (forbidding rewriting a term reduced to an evar)
herbelin
2010-04-05
*
Tests for bug report #2244 (pattern-unification with abstraction over Meta's)
herbelin
2010-04-05
*
Applied greenrd's patch to fix bug 2255 (injection failed to
herbelin
2010-03-27
*
bugs/.../1784.v: revert Matthieu's recent fix, since Program has been made co...
letouzey
2010-02-10
*
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
*
Fix test-suite scripts: [Generalizable Variables] and small
msozeau
2009-11-13
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
- 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
*
Fix wrong pattern in Morphisms. Fix bug scripts to reflect the fact that
msozeau
2009-04-20
*
Fix bug #2089: correctly dealing with parameters and real arguments in
msozeau
2009-04-16
*
Fix and actually beautify the bug script to adapt to the new measure
msozeau
2009-04-14
*
Avoid inadvertent declaration of "on" as a keyword. New syntax is
msozeau
2009-03-29
*
Fixes in Program well-founded definitions:
msozeau
2009-03-26
*
Fixing bug #1918 (no occur-check in Meta unification was done yet!).
herbelin
2009-01-20
*
- Fixing bug 1891 (abusive instantiations of evar arguments in
herbelin
2009-01-20
*
Backporting from v8.2 to trunk:
herbelin
2009-01-18
*
Fix a bunch of bugs related to setoid_rewrite, unification and evars:
msozeau
2009-01-12
*
- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).
herbelin
2009-01-11
*
Fixed bugs #2001 (search_guard was overwriting the guard index given
herbelin
2009-01-04
*
- Fixed bug #2021 (uncaught exception with injection/discriminate when
herbelin
2009-01-01
*
Finish fix for the treatment of [inverse] in [setoid_rewrite], making a
msozeau
2008-12-16
*
fixed bug 1791: simpl was performing eta expansion
barras
2008-11-27
*
closed bug 1898: fold x in x; added a reordering primitive tactic
barras
2008-11-26
*
Fixed bug #2006 (type constraint on Record was not taken into account) +
herbelin
2008-11-23
*
Add missing test-suite files for closed bugs.
msozeau
2008-11-14
[prev]
[next]