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
2019-04-23
Merge PR #9889: Fix pretty-printing of primitive integers
Maxime Dénès
2019-04-20
Merge PR #9906: coq_makefile install target: error if any file is missing
Enrico Tassi
2019-04-16
Fix spurious argument of {measure}
Maxime Dénès
2019-04-16
Take advantage of relaxed {measure} syntax in test suite
Maxime Dénès
2019-04-08
coq_makefile install target: error if any file is missing
Gaëtan Gilbert
2019-04-08
Merge PR #9900: [native compiler] Fix critical bug with stuck primitive proje...
Pierre-Marie Pédrot
2019-04-06
Fix numeral notations test in async mode.
Gaëtan Gilbert
2019-04-06
Fix pretty-printing of primitive integers
Erik Martin-Dorel
2019-04-05
[native compiler] Fix critical bug with primitive projections
Maxime Dénès
2019-04-05
Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)
Emilio Jesus Gallego Arias
2019-04-03
Merge PR #8638: Remove -compat 8.7
Théo Zimmermann
2019-04-02
Merge PR #8984: Declare initial hint databases in prelude
Pierre-Marie Pédrot
2019-04-02
Remove -compat 8.7
Jason Gross
2019-04-02
Merge PR #9659: Fix #9652: rewrite fails to detect lack of progress
Emilio Jesus Gallego Arias
2019-04-02
Add a Numeral Notation for QArith (e.g., 1.02e+01%Q for 102 # 10)
Pierre Roux
2019-04-02
Make R parser parse decimals (e.g., 1.02e+01)
Pierre Roux
2019-04-02
Add parsing of decimal constants (e.g., 1.02e+01)
Pierre Roux
2019-04-01
Merge PR #9725: Lia: various impovements (support for #8764, fix #9268 and ...
Vincent Laporte
2019-04-01
Add test-case for #9840
Jason Gross
2019-04-01
Several improvements and fixes of Lia
Frédéric Besson
2019-04-01
Merge PR #9872: Fix timing diff script to support non-utf8
Emilio Jesus Gallego Arias
2019-03-31
[pretty-timing scripts] Don't barf on non-utf-8
Jason Gross
2019-03-30
Error when [foo.(bar)] is used with nonprojection [bar]
Gaëtan Gilbert
2019-03-28
Merge PR #9743: Relax the ambiguous path condition of coercion
Enrico Tassi
2019-03-27
Merge PR #9837: Fix some critical-bugs informations
Théo Zimmermann
2019-03-26
Fix reproduction info for some past critical bugs
Gaëtan Gilbert
2019-03-26
Merge PR #9690: Fix 9663 (Miller pattern unification fails on evars)
Matthieu Sozeau
2019-03-26
Merge PR #9489: [ssr] avoid HO unification to perform truncation analysy in elim
Maxime Dénès
2019-03-26
[evarconv] solve_simple_eqn is weaker than miller pattern (fix #9663)
Enrico Tassi
2019-03-26
Declare initial hint databases in prelude
Maxime Dénès
2019-03-25
[ssr] avoid HO unif when doing truncation analysis
Enrico Tassi
2019-03-25
Fix #9652: rewrite fails to detect lack of progress
Gaëtan Gilbert
2019-03-22
Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ...
Maxime Dénès
2019-03-20
Merge PR #9776: [kernel] Fix compare_head_gen_leq_with to use [leq] on applic...
Gaëtan Gilbert
2019-03-20
Merge PR #8669: Show diffs in some error messages
Emilio Jesus Gallego Arias
2019-03-18
[kernel] Fix compare_head_gen_leq_with to use [leq] on applications
Matthieu Sozeau
2019-03-14
Relax the ambiguous path condition of coercion
Kazuhiko Sakaguchi
2019-03-14
Documentation for SProp
Gaëtan Gilbert
2019-03-14
Test for SkySkimmer/coq#13
Gaëtan Gilbert
2019-03-14
Repair relevance marks in-kernel.
Gaëtan Gilbert
2019-03-14
Enable proof irrelevance for SProp.
Gaëtan Gilbert
2019-03-14
Inductives in SProp, forbid primitive records with only sprop fields
Gaëtan Gilbert
2019-03-14
Add relevance marks on binders.
Gaëtan Gilbert
2019-03-14
Add a non-cumulative impredicative universe SProp.
Gaëtan Gilbert
2019-03-14
Fix Require in output test for reals syntax
Gaëtan Gilbert
2019-03-13
Merge PR #9736: Don't coqchk the test suite prerequisites
Enrico Tassi
2019-03-12
Merge PR #9632: Fix #9631: Instance: anomaly grounding non evar-free term
Emilio Jesus Gallego Arias
2019-03-12
Merge PR #9596: Fix #9595: missing non-primitive-record warning with 0 field ...
Emilio Jesus Gallego Arias
2019-03-12
Merge PR #9389: Implement a method for manual declaration of implicits.
Emilio Jesus Gallego Arias
2019-03-11
Don't coqchk the test suite prerequisites
Gaëtan Gilbert
[next]