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
2020-01-29
Merge PR #11399: Checker: use inductive's check_template flag
Pierre-Marie Pédrot
2020-01-29
Merge PR #11472: Fix #11467 ('e' was not displayed when printing decimal nota...
Pierre-Marie Pédrot
2020-01-28
Fix #11467
Pierre Roux
2020-01-27
Checker: use inductive's check_template flag
Gaëtan Gilbert
2020-01-27
schemes: use rigid universes
Gaëtan Gilbert
2020-01-22
Fix #11421 computation of Set+2
Gaëtan Gilbert
2020-01-19
Merge PR #11368: Turn trailing implicit warning into an error
Hugo Herbelin
2020-01-19
Merge PR #11348: Discharge inductive types without rechecking them
Pierre-Marie Pédrot
2020-01-17
Merge PR #11362: Lia bugfix 11191
Maxime Dénès
2020-01-15
Merge PR #11373: Close #11168
Pierre-Marie Pédrot
2020-01-15
Merge PR #11374: Close #11133
Pierre-Marie Pédrot
2020-01-15
Discharge inductive types without rechecking them
Gaëtan Gilbert
2020-01-14
Merge PR #11394: [coqdoc] Fix #11353: coqdoc -g omits all sentences with deco...
Hugo Herbelin
2020-01-14
[coqdoc] Fix #11353: coqdoc -g omits all sentences with decorations
Karl Palmskog
2020-01-14
Merge PR #10486: [extraction] Support extraction of Coq's string type to OCam...
Kazuhiko Sakaguchi
2020-01-13
Merge PR #11285: fix #11279. Specialize h no longer expands letins in the typ...
Pierre-Marie Pédrot
2020-01-13
Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and...
Pierre-Marie Pédrot
2020-01-12
fix #11279. Specialize h no longer expands letins in the type of h.
Pierre Courtieu
2020-01-09
Merge PR #11164: [CS] allow Let variable to be canonical
Pierre-Marie Pédrot
2020-01-08
Add test case for string extraction in OCaml and Haskell
Maxime Dénès
2020-01-08
Close #11133
Gaëtan Gilbert
2020-01-08
replace deprecated -quick with -vio in the test suite
Enrico Tassi
2020-01-08
Close #11168
Gaëtan Gilbert
2020-01-08
Merge PR #11341: Add non-utf8 timing test
Pierre-Marie Pédrot
2020-01-07
Merge PR #11245: [tools] Remove support for python2
Théo Zimmermann
2020-01-07
Fix test-suite fo non maximal implicit arguments
SimonBoulier
2020-01-06
Fix #11140: Bidirectionality hints perform (surprising?) simplification
Maxime Dénès
2020-01-06
[micromega] fix of bug #11191
Frédéric Besson
2020-01-06
Merge PR #11361: Fix #11360: discharge of template inductive with param only ...
Pierre-Marie Pédrot
2020-01-06
Fix #11360: discharge of template inductive with param only use of var
Gaëtan Gilbert
2020-01-04
Fixing status reporting for complexity tests.
Hugo Herbelin
2020-01-03
Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issue
Enrico Tassi
2020-01-03
coq_makefile: test with CAMLPKGS and mllib
Gaëtan Gilbert
2020-01-03
[tools] Remove support for python2
Emilio Jesus Gallego Arias
2019-12-30
Merge PR #11233: Fixes #11231: missing dependency in looking for default clau...
Pierre-Marie Pédrot
2019-12-29
Merge PR #11334: Fixes a small bug exposing an _ANONYMOUS_REL in a unificatio...
Pierre-Marie Pédrot
2019-12-28
Merge PR #11323: Fix mulc on 32-bit architectures
Michael Soegtrop
2019-12-28
Extend `Print Canonical Projections` with a search functionality
Kazuhiko Sakaguchi
2019-12-27
Add critical-bugs entry, tests-suite file, and code comment.
Guillaume Melquiond
2019-12-27
Merge PR #11315: Ensure that a custom entry cannot be defined twice.
Hugo Herbelin
2019-12-27
fix: Shorten ssrsetoid.v
Erik Martin-Dorel
2019-12-26
Add non-utf8 timing test
Jason Gross
2019-12-26
Deprecate the "omega with *" syntax.
Pierre-Marie Pédrot
2019-12-24
[Attributes] accept #[canonical] (Let|Definition)
Enrico Tassi
2019-12-24
[CS] Allow a variable introduced with Let to be a canonical instance
Enrico Tassi
2019-12-23
Fixes a small bug exposing an _ANONYMOUS_REL in a unification error message.
Hugo Herbelin
2019-12-23
Merge PR #10760: Make rapply handle all numbers of underscores
Pierre-Marie Pédrot
2019-12-22
Ensure that a custom entry cannot be defined twice.
Pierre-Marie Pédrot
2019-12-21
Merge PR #11311: Fix handling of recursive notations with custom entries
Hugo Herbelin
2019-12-20
Merge PR #11308: Fix complexity test-suite failure reporting on Win
Enrico Tassi
[next]