index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
output
/
Cases.v
Commit message (
Expand
)
Author
Age
*
Introduce an option to allow nested lemma, and turn it off by default.
Théo Zimmermann
2018-05-17
*
In printing, factorizing "match" clauses with same right-hand side.
Hugo Herbelin
2017-12-12
*
A fix to #5414 (ident bound by ltac names now known for "match").
Hugo Herbelin
2017-06-09
*
Better support for printing constructors with let-ins.
Hugo Herbelin
2017-04-07
*
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-10-19
*
Fix issues in test-suite revealed by warnings.
Maxime Dénès
2016-06-29
*
Using x in output test-suite Cases.v (cosmetic).
Hugo Herbelin
2015-12-05
*
Updating test-suite after Bracketing Last Introduction Pattern set by
Hugo Herbelin
2015-11-10
*
Fixing clash in output test-suite Cases.
Hugo Herbelin
2014-10-23
*
A patch for printing "match" when constructors are defined with let-in
Hugo Herbelin
2014-10-20
*
Fixing #3293 (eta-expansion at "match" printing time was failing
Hugo Herbelin
2014-04-28
*
Parameters in pattern first step.
pboutill
2012-01-16
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Test case for previous commit.
msozeau
2008-11-27
*
Correction de quelques défauts d'affichage (notations sous "as" pour
herbelin
2007-10-05
*
- Fixing bug 1703 ("intros until n" falls back on the variable name when
herbelin
2007-09-21
*
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2005-12-21
*
Problème de désynchronisation des variables du type et du corps d'un point-...
herbelin
2003-01-15