index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
output
Age
Commit message (
Expand
)
Author
2020-02-08
Merge PR #11240: Add rew dependent Notations
Hugo Herbelin
2020-02-06
Merge PR #10835: Accepting a few more variants of format for recursive notati...
Pierre-Marie Pédrot
2020-01-31
More tolerant in format for recursive notations.
Hugo Herbelin
2020-01-30
Printing tests for applied references combined with impl. args. and notations.
Hugo Herbelin
2020-01-28
Fix #11467
Pierre Roux
2020-01-14
Merge PR #10486: [extraction] Support extraction of Coq's string type to OCam...
Kazuhiko Sakaguchi
2020-01-13
Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and...
Pierre-Marie Pédrot
2020-01-08
Add test case for string extraction in OCaml and Haskell
Maxime Dénès
2020-01-08
replace deprecated -quick with -vio in the test suite
Enrico Tassi
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
Extend `Print Canonical Projections` with a search functionality
Kazuhiko Sakaguchi
2019-12-26
Add rew dependent Notations
Jason Gross
2019-12-23
Fixes a small bug exposing an _ANONYMOUS_REL in a unification error message.
Hugo Herbelin
2019-12-20
Coherence checking for coercions
Kazuhiko Sakaguchi
2019-12-18
Merge PR #11203: Make the string argument of `time` print correctly
Pierre-Marie Pédrot
2019-12-17
[micromega] fix efficiency regression
Frédéric Besson
2019-12-06
Make the string argument of `time` print correctly
Jason Gross
2019-12-03
Printing: Interleaving search for notations and removal of coercions.
Hugo Herbelin
2019-12-03
Fixes #11231 (missing dependency in pattern-matching decompilation).
Hugo Herbelin
2019-11-29
Merge PR #11076: Remove all remaining calls to “omega” from the standard ...
Emilio Jesus Gallego Arias
2019-11-26
Merge PR #11090: Printing of coercions to which a notation is associated: a r...
Emilio Jesus Gallego Arias
2019-11-25
Test-suite: avoid using “omega”
Vincent Laporte
2019-11-21
A refined version of #8890 which prevents #11033.
Hugo Herbelin
2019-11-20
Combine similar arguments when printing Arguments command
Gaëtan Gilbert
2019-11-11
Miscellaneous improvements of the syntax of records.
Hugo Herbelin
2019-11-01
Add extraction for primitive floats
Erik Martin-Dorel
2019-11-01
Make primitive float work on Windows
Pierre Roux
2019-11-01
Pretty-printing primitive float constants
Erik Martin-Dorel
2019-10-31
Merge PR #10985: Print argument info as an Arguments command in About
Emilio Jesus Gallego Arias
2019-10-31
Merge PR #9883: Add support for Sorts in numeral notations
Vincent Laporte
2019-10-31
restore red behaviour printing
Gaëtan Gilbert
2019-10-31
Fix output tests
Gaëtan Gilbert
2019-10-29
`assert_succeeds`&`assert_fails`: multisuccess fix
Jason Gross
2019-10-28
Add support for Sorts in numeral notations
Jason Gross
2019-10-17
Fix Locate printing regression
Guillaume Melquiond
2019-10-14
Merge PR #10811: Allow SProp default on
Pierre-Marie Pédrot
2019-10-05
Fix #10669 incorrect substitution in context outside section
Gaëtan Gilbert
2019-10-04
Allow SProp default on
Gaëtan Gilbert
2019-09-16
Re-implementation of zify
Frédéric Besson
2019-09-09
[stdlib] Do not put INR_eq in the “real” hint database
Vincent Laporte
2019-09-04
Merge PR #10577: Fix #7348: extraction of dependent record projections
Maxime Dénès
2019-09-04
Merge PR #10612: Fix feedback levels
Emilio Jesus Gallego Arias
2019-09-02
Merge PR #10648: [extraction] Fix #7191: Avoid unsound eta-reduction
Maxime Dénès
2019-08-29
Make sure that all query commands return a notice (not an info) feedback
Maxime Dénès
2019-08-26
Make kernel parametric on the lowest universe and fix #9294
Matthieu Sozeau
2019-08-10
[extraction] Fix #7191: Avoid unsound eta-reduction
Kazuhiko Sakaguchi
2019-08-08
Fix regression of #10637 (-emacs arg sets color to `EMACS)
Jim Fehrle
2019-07-31
Fix #7348: extraction of dependent record projections
Kazuhiko Sakaguchi
2019-07-02
Improve the ambiguous paths warning to indicate which path is ambiguous with ...
Kazuhiko Sakaguchi
[next]