index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
success
/
intros.v
Commit message (
Expand
)
Author
Age
*
Make "intro"/"intros" progress on existential variables.
Hugo Herbelin
2018-05-02
*
Moving bug numbers to BZ# format in the test-suite.
Théo Zimmermann
2017-10-19
*
Stronger invariants on the use of the introduction pattern (pat1,...,patn).
Hugo Herbelin
2016-01-21
*
Fixing a bug with introduction patterns over inductive types containing let-ins.
Hugo Herbelin
2016-02-18
*
Fixing a bug in the order of side conditions for introduction pattern -> and <-.
Hugo Herbelin
2015-12-25
*
Fixing a pat%constr bug. Thanks to Enrico for reporting.
Hugo Herbelin
2015-12-10
*
Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.
Hugo Herbelin
2015-12-10
*
Improving syntax of pat/constr introduction pattern so that
Hugo Herbelin
2015-12-02
*
In pat/constr introduction patterns, fixing in a better way clearing problems
Hugo Herbelin
2015-09-16
*
Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commits
Hugo Herbelin
2015-09-08
*
Ensuring that patterns of the form pat/constr move the hypotheses replacing
Hugo Herbelin
2015-09-08
*
Seeing IntroWildcard as an action intro pattern rather than as a naming pattern
Hugo Herbelin
2014-09-30
*
Fixing introduction patterns * and ** when used in a branch so that they do n...
Hugo Herbelin
2014-05-31
*
Using hnf instead of "intro H" for forcing reduction to a product.
herbelin
2013-03-21
*
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2005-12-21