index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
output
/
Cases.v
Age
Commit message (
Expand
)
Author
2020-12-09
Fixing support for argument scopes and let-ins while interning cases patterns.
Hugo Herbelin
2020-10-05
Wish #12762: warning on duplicated catch-all pattern with unused named variable.
Hugo Herbelin
2019-12-03
Fixes #11231 (missing dependency in pattern-matching decompilation).
Hugo Herbelin
2019-08-26
Make kernel parametric on the lowest universe and fix #9294
Matthieu Sozeau
2018-12-19
Put #[universes(template)] in outputs tests
Gaëtan Gilbert
2018-10-04
test-suite: cleaning
Vincent Laporte
2018-07-25
In "redundant clause" pattern-matching error, show also the pattern (#7777).
Hugo Herbelin
2018-05-17
Introduce an option to allow nested lemma, and turn it off by default.
Théo Zimmermann
2017-12-12
In printing, factorizing "match" clauses with same right-hand side.
Hugo Herbelin
2017-06-09
A fix to #5414 (ident bound by ltac names now known for "match").
Hugo Herbelin
2017-04-07
Better support for printing constructors with let-ins.
Hugo Herbelin
2016-10-19
Test for variant of #5142 (good error message on pattern-matching failure).
Hugo Herbelin
2016-10-19
Attempt to improve error rendering in pattern-matching compilation (#5142).
Hugo Herbelin
2016-06-29
Fix issues in test-suite revealed by warnings.
Maxime Dénès
2015-12-05
Using x in output test-suite Cases.v (cosmetic).
Hugo Herbelin
2015-11-10
Updating test-suite after Bracketing Last Introduction Pattern set by
Hugo Herbelin
2014-10-23
Fixing clash in output test-suite Cases.
Hugo Herbelin
2014-10-20
A patch for printing "match" when constructors are defined with let-in
Hugo Herbelin
2014-04-28
Fixing #3293 (eta-expansion at "match" printing time was failing
Hugo Herbelin
2012-01-16
Parameters in pattern first step.
pboutill
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2008-11-27
Test case for previous commit.
msozeau
2007-10-05
Correction de quelques défauts d'affichage (notations sous "as" pour
herbelin
2007-09-21
- Fixing bug 1703 ("intros until n" falls back on the variable name when
herbelin
2005-12-21
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2003-01-15
Problème de désynchronisation des variables du type et du corps d'un point-...
herbelin
