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
*
Adding test for bug 3792.
Pierre-Marie Pédrot
2014-11-09
*
Follow up to experimental eager evar unification in bcba6d1bc9:
Hugo Herbelin
2014-11-08
*
Compatibility with 8.4 in the heuristic used to build the induction
Hugo Herbelin
2014-11-08
*
Test #3655 was failing due to an anomaly. Now it rather has to fail
Hugo Herbelin
2014-11-08
*
Test fixed by PMP's commits from Oct 21.
Hugo Herbelin
2014-11-08
*
Test for #3675 on primitive projections.
Hugo Herbelin
2014-11-07
*
Fixing #3562 ("as" in "destruct" expects either a disjunctive
Hugo Herbelin
2014-11-07
*
Test for #3542 fixed some time ago.
Hugo Herbelin
2014-11-07
*
Consequence of changing the definition of Nat.shiftl and Nat.shiftr.
Hugo Herbelin
2014-11-06
*
Restoring clear_flag (thanks a lot to jonikelee to notice it).
Hugo Herbelin
2014-11-06
*
Optimizing when to clear generalized hypotheses in destruct.
Hugo Herbelin
2014-11-06
*
Test for bug #3723 and #3787 on reinitialization of empty camlp4/5 levels.
Hugo Herbelin
2014-11-06
*
Removing "destruct" test not yet working.
Hugo Herbelin
2014-11-06
*
test suite: some reproduction cases for recently-reported bugs.
Xavier Clerc
2014-11-04
*
Test for bug #2149.
Pierre-Marie Pédrot
2014-11-04
*
New bugs revealed fixed: #3408 by (probably) Maxime's commits
Hugo Herbelin
2014-11-03
*
Subtle swap of lines to preserve VarInstance src field before checking
Hugo Herbelin
2014-11-03
*
Fix to 844431761 on improving elimination with indices, getting rid of
Hugo Herbelin
2014-11-03
*
Improving elimination with indices, getting rid of intrusive residual
Hugo Herbelin
2014-11-02
*
Some reorganization of the code for destruct/induction:
Hugo Herbelin
2014-11-02
*
Fixing file destruct.v.
Hugo Herbelin
2014-11-02
*
Enlarge the cases where the like first selection is used in destruct.
Hugo Herbelin
2014-10-31
*
Listing a few examples of destruct showing unsatisfactory behaviors.
Hugo Herbelin
2014-10-31
*
Avoid "destruct H" to apply on H itself when H is a section variable.
Hugo Herbelin
2014-10-31
*
Making destruct on idents with maximal implicit arguments working, by
Hugo Herbelin
2014-10-27
*
Ensuring compatibility when an hypothesis used for destruct is
Hugo Herbelin
2014-10-27
*
Fixing clash in test destruct.v.
Hugo Herbelin
2014-10-27
*
Fixing destruct/induction with a using clause on a non-inductive type,
Hugo Herbelin
2014-10-26
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
Fixing clash in output test-suite Cases.
Hugo Herbelin
2014-10-23
*
Taking into account factorization of consecutive names of same types
Hugo Herbelin
2014-10-23
*
Fixing typo in output test Notations.
Hugo Herbelin
2014-10-22
*
Fix test-suite for #2729.
Maxime Dénès
2014-10-22
*
Fixing an evar leak in pattern-matching compilation (#3758).
Hugo Herbelin
2014-10-22
*
Adapting output tests to the removal of the new token warning and to
Hugo Herbelin
2014-10-21
*
More precise test for #3459.
Hugo Herbelin
2014-10-21
*
Fixing a (new) part of bug #2729.
Hugo Herbelin
2014-10-20
*
A patch for printing "match" when constructors are defined with let-in
Hugo Herbelin
2014-10-20
*
Fixing a bug in the presence of let-in in inductive arity.
Hugo Herbelin
2014-10-20
*
Relaxing again the test on types of replacements in tactic change
Hugo Herbelin
2014-10-16
*
Fix test-suite scripts.
Matthieu Sozeau
2014-10-16
*
Bug fixed by Hugo.
Matthieu Sozeau
2014-10-16
*
Adding a timeout to bug #2447.
Pierre-Marie Pédrot
2014-10-15
*
To stay closer to non-primitive projections, only unfold primitive
Matthieu Sozeau
2014-10-15
*
Fix for bug #3618.
Matthieu Sozeau
2014-10-15
*
Closed bug 3710.
Matthieu Sozeau
2014-10-15
*
Bug 3692 is fixed.
Matthieu Sozeau
2014-10-15
*
Bug 3628 is fixed.
Matthieu Sozeau
2014-10-15
*
Fix test-suite files which failed due to usage of $(admit)$ which
Matthieu Sozeau
2014-10-15
*
Fix bug 3637.
Matthieu Sozeau
2014-10-15
[next]