coq - The formal proof system

Age	Commit message (Expand)	Author
2021-01-18	Preventing internal temporary names to impact the "?H"-like intro-pattern names.	Hugo Herbelin
2018-05-02	Make "intro"/"intros" progress on existential variables.	Hugo Herbelin
2017-10-19	Moving bug numbers to BZ# format in the test-suite.	Théo Zimmermann
2016-01-21	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin
2016-02-18	Fixing a bug with introduction patterns over inductive types containing let-ins.	Hugo Herbelin
2015-12-25	Fixing a bug in the order of side conditions for introduction pattern -> and <-.	Hugo Herbelin
2015-12-10	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-02	Improving syntax of pat/constr introduction pattern so that	Hugo Herbelin
2015-09-16	In pat/constr introduction patterns, fixing in a better way clearing problems	Hugo Herbelin
2015-09-08	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
2014-09-30	Seeing IntroWildcard as an action intro pattern rather than as a naming pattern	Hugo Herbelin
2014-05-31	Fixing introduction patterns * and ** when used in a branch so that they do n...	Hugo Herbelin
2013-03-21	Using hnf instead of "intro H" for forcing reduction to a product.	herbelin
2005-12-21	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin