index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
Age
Commit message (
Expand
)
Author
2014-11-25
Tweak some test cases.
Xavier Clerc
2014-11-25
Adapting to current semantics of "simpl non-evaluable-cst"
Hugo Herbelin
2014-11-25
Experimenting using unification when matching evar/meta free subterms
Hugo Herbelin
2014-11-24
Adding test for bug #3248.
Pierre-Marie Pédrot
2014-11-23
Pass around information on the use of template polymorphism for
Matthieu Sozeau
2014-11-22
Test for closed #2713 and #2876.
Hugo Herbelin
2014-11-22
Add test-suite file for dependent rewriting example by Vadim Zaliva and
Matthieu Sozeau
2014-11-21
Adding test for bug #3326.
Pierre-Marie Pédrot
2014-11-21
Adding test for bug #3424.
Pierre-Marie Pédrot
2014-11-21
Cleaning up closed bugs in test-suite.
Pierre-Marie Pédrot
2014-11-21
Test for bug #3788.
Pierre-Marie Pédrot
2014-11-21
Add test-suite file for bug #3804.
Matthieu Sozeau
2014-11-20
Adding test for bug #3684.
Pierre-Marie Pédrot
2014-11-18
Fixing a little bug with nested but convertible occurrences in "destruct at".
Hugo Herbelin
2014-11-18
Fixing detection of occurrences in the presence of nested subterms for
Hugo Herbelin
2014-11-16
Enforcing a stronger difference between the two syntaxes "simpl
Hugo Herbelin
2014-11-16
Fixing side bug in db37c9f3f32ae7 delaying interpretation of the
Hugo Herbelin
2014-11-14
Use return code to classify anomalies as active open bugs.
Xavier Clerc
2014-11-14
Add missing "Fail" to test case for bug #2814.
Xavier Clerc
2014-11-14
Reproduction cases for the test suite.
Xavier Clerc
2014-11-14
Preserving the good effect of 014e5ac92a on not leaving dangling local
Hugo Herbelin
2014-11-13
Removing yet another source of remaining local definitions.
Hugo Herbelin
2014-11-11
Adapting output tests to current naming of evars, even if unclear
Hugo Herbelin
2014-11-09
Adding test for bug 3792.
Pierre-Marie Pédrot
2014-11-08
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-07
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-06
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-04
test suite: some reproduction cases for recently-reported bugs.
Xavier Clerc
2014-11-04
Test for bug #2149.
Pierre-Marie Pédrot
2014-11-03
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-02
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-10-31
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-27
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
[next]