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
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-20
|
\
|
*
Fix bug #4737: cycle tactic doesn't like zero goals.
Pierre-Marie Pédrot
2016-05-16
*
|
STM: code cleanup
Enrico Tassi
2016-05-10
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-09
|
\
|
|
*
Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.
Pierre-Marie Pédrot
2016-05-08
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
|
\
|
|
*
Fixing subst.out after changing spacing in goal output (24a125b77).
Hugo Herbelin
2016-05-04
|
*
Handle primitive projections inside types when extracting (bug #4616).
Guillaume Melquiond
2016-05-04
|
*
In Regular Subst Tactic mode, ensure that the order of hypotheses is
Hugo Herbelin
2016-05-03
|
*
Fix bug #3825: Universe annotations on notations should pass through or be re...
Pierre-Marie Pédrot
2016-05-03
|
*
Test file for #4695: Slow Qed.
Maxime Dénès
2016-05-03
|
*
Fix bug #4292: Unexpected functor objects.
Pierre-Marie Pédrot
2016-05-03
|
*
Use the canonical name when looking for an eliminator (bug #4670).
Guillaume Melquiond
2016-05-03
|
*
Call hooks when terminating a definition proof (bug #4663).
Guillaume Melquiond
2016-05-03
|
*
Remove extraneous space in coqtop/pg output (bug #4675).
Guillaume Melquiond
2016-05-03
|
*
Properly handle notations containing spaces (bug #4538).
Guillaume Melquiond
2016-05-02
|
*
Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).
Guillaume Melquiond
2016-05-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-02
|
\
|
|
*
Fix incorrect cbv reduction of primitive projections. (Bug #4634)
Guillaume Melquiond
2016-04-29
|
*
An example for cd139311e, showing a consequence of not converting
Hugo Herbelin
2016-04-28
*
|
Revert "A heuristic to add parentheses in the presence of rules such as"
Hugo Herbelin
2016-04-27
*
|
A heuristic to add parentheses in the presence of rules such as
Hugo Herbelin
2016-04-27
*
|
Fixing a "This clause is redundant" error when interpreting the "in"
Hugo Herbelin
2016-04-27
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-24
|
\
|
|
*
Fixing output test Notations2.
Hugo Herbelin
2016-04-22
*
|
Do that "make" in test-suite writes failures as a default together
Hugo Herbelin
2016-04-19
|
*
Fixing #4677 (collision of a global variable and of a local variable
Hugo Herbelin
2016-04-19
|
*
Quick fix for #4603 (part 2): Anomaly: Universe undefined
Maxime Dénès
2016-04-12
*
|
A small test of Print Ltac.
Hugo Herbelin
2016-04-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-09
|
\
|
*
|
Fixing printing of Tactic Notations with tactic arguments.
Pierre-Marie Pédrot
2016-04-08
|
*
Allow to unset the refinement mode of Instance in ML
Matthieu Sozeau
2016-04-07
*
|
An example which failed in 8.5 and that d670c6b6 fixes.
Hugo Herbelin
2016-04-07
|
*
Add -compat 8.4 econstructor tactics, and tests
Jason Gross
2016-04-05
|
*
Fix bug #4656
Jason Gross
2016-04-05
*
|
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...
Matthieu Sozeau
2016-04-04
|
\
\
*
|
|
Adding a test for bug #1850.
Pierre-Marie Pédrot
2016-03-31
*
|
|
Fixing an incorrect use of prod_appvect on a term which was not a
Hugo Herbelin
2016-03-28
*
|
|
Test suite file for a bug in BigQ arithmetic fixed a while ago.
Maxime Dénès
2016-03-25
*
|
|
Test suite file for a bug in int31 arithmetic fixed a while ago.
Maxime Dénès
2016-03-25
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-20
|
\
\
\
|
|
|
/
|
|
/
|
*
|
|
Moving the parsing of the Ltac proof mode to G_ltac.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-18
|
\
\
\
|
|
*
|
Fix bug #4627: records with no declared arity can be template polymorphic.
Matthieu Sozeau
2016-03-17
|
|
*
|
Test file for #4623.
Maxime Dénès
2016-03-17
|
|
*
|
Test file for #4624, fixed by Matthieu's bfce815bd1.
Maxime Dénès
2016-03-16
|
|
/
/
|
*
|
Fix bug when a sort is ascribed to a Record
Matthieu Sozeau
2016-03-15
*
|
|
Adopting the same rules for interpreting @, abbreviations and
Hugo Herbelin
2016-03-13
*
|
|
Adding a file summarizing the inconsistencies in interpreting implicit
Hugo Herbelin
2016-03-13
|
*
|
According to Bruno, my fix for #4588 seems to be enough.
Maxime Dénès
2016-03-11
[next]