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
*
Notations are back in the "in" clause of pattern matching.
pboutill
2012-05-15
*
Implicit arguments of Definition are taken from the type when given by the user.
pboutill
2012-04-27
*
remove undocumented and scarcely-used tactic auto decomp
letouzey
2012-04-23
*
Bug 2733 : { } implicits and Fixpoints
pboutill
2012-04-17
*
Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).
herbelin
2012-04-15
*
Repair two tests
letouzey
2012-04-12
*
Fixing a few bugs (see #2571) related to interpretation of multiple binders
herbelin
2012-04-06
*
Relax uniform inheritance condition
gareuselesinge
2012-04-05
*
Unification: Added a heuristic to solve problems of the form
herbelin
2012-03-26
*
Fix the test-suite by removing any Reset in the scripts
letouzey
2012-03-23
*
evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structures
gareuselesinge
2012-03-22
*
Fixing bug #2724 (using notations with binders in cases patterns
herbelin
2012-03-20
*
Fixing alpha-conversion bug #2723 introduced in r12485-12486.
herbelin
2012-03-20
*
Generalized the use of evar candidates in type inference unification:
herbelin
2012-03-20
*
Fix bugs related to Program integration.
msozeau
2012-03-19
*
Fixing bug #2732 (anomaly when using the tolerance for writing
herbelin
2012-03-18
*
Fixing vm_compute bug #2729 (function used to decompose constructors
herbelin
2012-03-13
*
"Let in" in pattern hell, one more iteration
pboutill
2012-03-02
*
Noise for nothing
pboutill
2012-03-02
*
Use a heuristic to not simplify equality hypotheses remaining after dependent...
msozeau
2012-02-20
*
Arguments supports extra notation scopes
gareuselesinge
2012-02-14
*
Fix consequence of pp bugfix in testsuite
pboutill
2012-01-31
*
Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...
msozeau
2012-01-28
*
Notations with binders: Accepting using notations for functional terms
herbelin
2012-01-20
*
Parameters in pattern first step.
pboutill
2012-01-16
*
Add distclean back to test-suite/Makefile
glondu
2012-01-14
*
Backtracking on r14876 (fix for bug #2267): extra scopes might be
herbelin
2012-01-05
*
Fixing Arguments Scope bug when too many scopes are given (bug #2667).
herbelin
2012-01-04
*
Type inference unification: fixed a 8.4 bug in the presence of unification
herbelin
2012-01-04
*
Arguments: check rename even if no implicit is specified
gareuselesinge
2011-12-19
*
test suite update after r14808
pboutill
2011-12-19
*
Fixing bug #2634 (unscoped notations were disturbing the
herbelin
2011-12-18
*
Fixed a Not_found bug when declaring in a section some implicit
herbelin
2011-12-18
*
Added ability to take the type of applied metas into account when
herbelin
2011-12-17
*
Command Arguments: standardizing format of error messages and American spelling.
herbelin
2011-12-17
*
Bypassing the use of (currently unimplemented) "Show Script" in tests
herbelin
2011-12-17
*
Fixing format of complexity bug Notations.v.
herbelin
2011-12-17
*
Fixing amazing loop when using eta-expansion in pattern-matching for
herbelin
2011-12-16
*
Proof using ...
gareuselesinge
2011-12-12
*
Fixing grammar resetting bug in the presence of levels initially empty
herbelin
2011-12-07
*
Adapting test Existentials to new numbering strategy of evars (r14764).
herbelin
2011-12-07
*
Fixing a bug of commit r13310 (activating coercions only when module
herbelin
2011-12-07
*
Minor fixes to Arguments
gareuselesinge
2011-12-06
*
A small test for type inference (used to be a regression at some time).
herbelin
2011-12-04
*
Fixing superflous newline in output of About when no parameter is renamed.
herbelin
2011-12-04
*
Discarding let-ins from the instances of the evars in the
herbelin
2011-12-04
*
Quick hack to avoid anomaly on using Program w/o having required JMeq.
herbelin
2011-11-30
*
Extraction: Richer patterns in matchs as proposed by P.N. Tollitte
letouzey
2011-11-28
*
Fixed a bug in postprocessing dependencies in pattern-matching compilation
herbelin
2011-11-26
*
Renamig support added to "Arguments"
gareuselesinge
2011-11-21
[next]