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 a test-suite for the only printing flag.
Pierre-Marie Pédrot
2016-06-28
*
Shrink Proofs/Obligations by default and deprecate
Matthieu Sozeau
2016-06-27
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-27
|
\
*
|
Patterns in binders: printing tests
Arnaud Spiwack
2016-06-27
*
|
Patterns in binders: functional tests
Arnaud Spiwack
2016-06-27
*
|
Adding ability to put any pattern in binders, prefixed by a quote.
Daniel de Rauglaudre
2016-06-27
|
*
More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).
Hugo Herbelin
2016-06-27
*
|
Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).
Hugo Herbelin
2016-06-24
*
|
Test-suite fix to 1744e37 (injection in context).
Hugo Herbelin
2016-06-18
*
|
Adding an "as" clause to specialize.
Hugo Herbelin
2016-06-18
*
|
Giving a more natural semantics to injection by default.
Hugo Herbelin
2016-06-18
*
|
Exporting a generic argument induction_arg. As a consequence,
Hugo Herbelin
2016-06-18
*
|
par: like all: but in parallel
Enrico Tassi
2016-06-17
*
|
proof mode: print unification constraints
Matthieu Sozeau
2016-06-16
*
|
Tentative fix of test-suite file to avoid loop
Matthieu Sozeau
2016-06-16
*
|
Cleanup and refactoring
Matthieu Sozeau
2016-06-16
*
|
Revise syntax of Hint Cut
Matthieu Sozeau
2016-06-16
*
|
Example given at DeepSpec workshop
Matthieu Sozeau
2016-06-16
*
|
Purely refactoring and code/API cleanup.
Matthieu Sozeau
2016-06-16
*
|
eauto: fix test-suite file
Matthieu Sozeau
2016-06-16
*
|
bteauto: a Proofview.tactic for multiple goals
Matthieu Sozeau
2016-06-16
*
|
Fix iterative deepening strategy failing too early
Matthieu Sozeau
2016-06-16
*
|
Implement limited proof search and iterative deepening.
Matthieu Sozeau
2016-06-16
*
|
Typeclasses eauto based on new proof engine,
Matthieu Sozeau
2016-06-16
*
|
Refine 9cc95f5, unification of Let-In's, bug #3929
Matthieu Sozeau
2016-06-16
*
|
Not taking arguments given by name or position into account when
Hugo Herbelin
2016-06-16
*
|
Merge 'pr/191' into trunk
Enrico Tassi
2016-06-16
|
\
\
*
\
\
Merge branch 'pr/146' into trunk
Enrico Tassi
2016-06-16
|
\
\
\
*
|
|
|
Fix test-suite for opened bug #4813.
Pierre-Marie Pédrot
2016-06-15
|
*
|
|
Merge branch 'pr/146' into trunk
Enrico Tassi
2016-06-15
|
/
|
|
|
|
*
|
|
ssrmatching: simple test for Ltac API
Enrico Tassi
2016-06-15
*
|
|
|
fix test-suite/ide Makefile (stupid typo)
Enrico Tassi
2016-06-15
|
/
/
/
|
|
*
Merge branch 'bug4450' into v8.5
Matthieu Sozeau
2016-06-14
|
|
|
\
|
|
*
\
Merge branch 'bug4725' into v8.5
Matthieu Sozeau
2016-06-14
|
|
|
\
\
|
|
*
|
|
Admitted: fix #4818 return initial stmt and univs
Matthieu Sozeau
2016-06-14
*
|
|
|
|
test-suiet: run fake_id as before pr/173 was merged
Enrico Tassi
2016-06-14
*
|
|
|
|
Merge remote-tracking branch 'origin/pr/173' into trunk
Enrico Tassi
2016-06-14
|
\
\
\
\
\
|
|
*
|
|
|
Ident selectors cannot be used inside an Ltac expression.
Cyprien Mangin
2016-06-14
|
|
*
|
|
|
Goal selectors are now tacticals and can be used as such.
Cyprien Mangin
2016-06-14
|
|
*
|
|
|
Remove the need for brackets in goal selectors.
Cyprien Mangin
2016-06-14
|
|
*
|
|
|
Add test-suite file for goal selectors.
Cyprien Mangin
2016-06-14
|
|
/
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge branch "LtacProf for trunk" (PR #165).
Pierre-Marie Pédrot
2016-06-14
|
\
\
\
\
\
*
|
|
|
|
|
Univs: more robust Universe/Constraint decls #4816
Matthieu Sozeau
2016-06-13
|
|
|
*
|
|
Fix test-suite file, only part 2 is fixed in 8.5
Matthieu Sozeau
2016-06-13
*
|
|
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-13
|
\
\
\
\
\
\
|
|
|
|
*
|
|
Univs: fix for part #2 of bug #4816.
Matthieu Sozeau
2016-06-13
|
|
|
_
|
/
/
/
|
|
/
|
|
|
|
*
|
|
|
|
|
For the record, an example one would like to see working.
Hugo Herbelin
2016-06-12
|
*
|
|
|
|
Another fix to #4782 (a typing error not captured when dealing with bindings).
Hugo Herbelin
2016-06-12
|
*
|
|
|
|
Fixing #4782 (a typing error not captured when dealing with bindings).
Hugo Herbelin
2016-06-11
*
|
|
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-09
|
\
|
|
|
|
|
[next]