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
*
Merge PR #664: Fixing #5500 (missing test in return clause of match leading t...
Matthieu Sozeau
2018-06-14
|
\
*
\
Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder i...
Matthieu Sozeau
2018-06-14
|
\
\
*
|
|
Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").
Hugo Herbelin
2018-06-12
|
*
|
Fixes #7780 (missing lift in expanding alias under a binder in unification).
Hugo Herbelin
2018-06-12
|
/
/
*
|
Fixing #7700 (section variables bound to abbreviations were not found).
Hugo Herbelin
2018-06-10
*
|
Merge PR #7077: Preserving canonical structure of return predicate in vm_comp...
Maxime Dénès
2018-06-05
|
\
\
*
|
|
Fix #7631: native_compute fails to compile an example in Coq 8.8
Maxime Dénès
2018-06-04
|
*
|
Tests for part of #7068 and for #7076 (vm/native_compute and return predicate).
Hugo Herbelin
2018-06-04
|
/
/
*
|
Merge PR #7229: Deprecate implicit tactic solving.
Hugo Herbelin
2018-06-04
|
\
\
*
\
\
Merge PR #7199: Fixes #7195: missing freshness condition in Ltac pattern-matc...
Matthieu Sozeau
2018-06-04
|
\
\
\
*
\
\
\
Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.
Matthieu Sozeau
2018-06-04
|
\
\
\
\
*
\
\
\
\
Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly
Matthieu Sozeau
2018-06-04
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #7189: Fix #5539: algebraic universe produced by cases.
Matthieu Sozeau
2018-06-04
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ta...
Matthieu Sozeau
2018-06-04
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".
Matthieu Sozeau
2018-06-04
|
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
*
|
Deprecate implicit tactic solving.
Pierre-Marie Pédrot
2018-06-04
|
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.
Maxime Dénès
2018-06-04
|
\
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
|
Fix #7113: Program Let Fixpoint in section causes anomaly
Gaëtan Gilbert
2018-05-30
*
|
|
|
|
|
|
|
|
Fix #6951: Unexpected error during scheme creation.
Pierre-Marie Pédrot
2018-05-29
|
|
_
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
Add test for #7333: vm_compute segfaults / Anomaly with cofix
Maxime Dénès
2018-05-29
|
|
*
|
|
|
|
|
Fix #7586: Anomaly "Uncaught exception Not_found".
Pierre-Marie Pédrot
2018-05-23
|
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
*
|
|
|
|
|
|
Add test cases from #7554
Tej Chajed
2018-05-20
*
|
|
|
|
|
|
Introduce an option to allow nested lemma, and turn it off by default.
Théo Zimmermann
2018-05-17
*
|
|
|
|
|
|
Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling s...
Gaëtan Gilbert
2018-05-14
|
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repo
Ralf Jung
2018-05-13
|
|
*
|
|
|
|
|
Fix #4403: insufficient handling of type-in-type in kernel.
Gaëtan Gilbert
2018-05-13
|
|
/
/
/
/
/
/
*
|
|
|
|
|
|
Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).
Hugo Herbelin
2018-05-10
*
|
|
|
|
|
|
Fixes part 1 of #7462 (only-printing not to override existing interp rule).
Hugo Herbelin
2018-05-10
|
/
/
/
/
/
/
*
|
|
|
|
|
[ltac] Deprecate nameless fix/cofix.
Emilio Jesus Gallego Arias
2018-04-13
*
|
|
|
|
|
Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by removin...
Jason Gross
2018-04-12
|
\
\
\
\
\
\
*
|
|
|
|
|
|
Fix the status of some resolved bugs
Tej Chajed
2018-04-11
|
|
|
|
|
*
|
Fixes #7195 (missing freshness condition in Ltac pattern-matching names).
Hugo Herbelin
2018-04-08
|
|
|
*
|
|
|
Fix #5539: algebraic universe produced by cases.
Gaëtan Gilbert
2018-04-06
|
|
|
|
|
/
/
|
|
|
|
/
|
|
*
|
|
/
|
|
Fix #6956: Uncaught exception in bytecode compilation
Maxime Dénès
2018-04-06
|
|
_
|
/
/
/
|
/
|
|
|
|
|
*
|
|
|
Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test.
Théo Zimmermann
2018-04-05
|
/
/
/
/
*
|
|
|
Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)
Pierre-Marie Pédrot
2018-04-01
|
\
\
\
\
*
|
|
|
|
Change Implicit Arguments to Arguments in test-suite
Jasper Hugunin
2018-03-30
|
|
|
*
|
Fix #6770: fixpoint loses locality info in proof mode.
Gaëtan Gilbert
2018-03-29
*
|
|
|
|
Fix #6631: Derive Plugin gives "Anomaly: more than one statement".
Pierre-Marie Pédrot
2018-03-29
|
|
_
|
/
/
|
/
|
|
|
|
*
|
|
Supporting fix/cofix in Ltac pattern-matching (wish #7092).
Hugo Herbelin
2018-03-28
|
/
/
/
|
|
*
Fixing #5547 (typability of return predicate in nested pattern-matching).
Hugo Herbelin
2018-03-27
|
|
*
Fixing #5500 (missing test in return clause of match leading to anomaly).
Hugo Herbelin
2018-03-27
|
|
/
|
/
|
|
*
Fixes #7011 (Fix/CoFix were not considered in tactic unification).
Hugo Herbelin
2018-03-26
|
/
*
Allow using cumulativity without forcing strict constraints.
Gaëtan Gilbert
2018-03-09
*
Merge PR #6895: [compat] Remove "Refolding Reduction" option.
Maxime Dénès
2018-03-09
|
\
*
|
More examples about shelve/given_up in tactic-in-terms.
Hugo Herbelin
2018-03-08
*
|
Proof engine: support for nesting tactic-in-term within other tactics.
Hugo Herbelin
2018-03-08
|
*
[compat] Remove "Refolding Reduction" option.
Emilio Jesus Gallego Arias
2018-03-08
|
/
*
Merge PR #6899: [compat] Remove "Standard Proposition Elimination"
Maxime Dénès
2018-03-08
|
\
*
\
Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)
Maxime Dénès
2018-03-08
|
\
\
[next]