coq - The formal proof system

Age	Commit message (Collapse)	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
	Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
2016-01-21	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin
	The length of the pattern should now be exactly the number of assumptions and definitions introduced by the destruction or induction, including the induction hypotheses in case of an induction. Like for pattern-matching, the local definitions in the argument of the constructor can be skipped in which case a name is automatically created for these.
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
	Marking it as experimental.
2015-12-02	Improving syntax of pat/constr introduction pattern so that	Hugo Herbelin
	pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat. Open to other suggestions of syntax though.
2015-09-16	In pat/constr introduction patterns, fixing in a better way clearing problems	Hugo Herbelin
	of temporary hypotheses than 76f27140e6e34 did.
2015-09-08	Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commits	Hugo Herbelin
	ago) which broke compilation of theories/Logic/WKL.v (collision between a temporary name and a user name).
2015-09-08	Ensuring that patterns of the form pat/constr move the hypotheses replacing	Hugo Herbelin
	an initial hypothesis hyp at the same position in the context. Ensuring the same for "apply c in hyp as pat". Ensuring that "pose proof (H ...) as H" does not change the position of H.
2014-09-30	Seeing IntroWildcard as an action intro pattern rather than as a naming pattern	Hugo Herbelin
	(the action is "clear"). Added subst_intropattern which was missing since the introduction of ApplyOn intro patterns. Still to do: make "intros _ ?id" working without interferences when "id" is precisely the internal name used for hypotheses to discard.
2014-05-31	Fixing introduction patterns * and ** when used in a branch so that they do ↵	Hugo Herbelin
	not introduce beyond what is under control of the branch. See test-suite intros.v for an example.
2013-03-21	Using hnf instead of "intro H" for forcing reduction to a product.	herbelin
	Added full betaiota in hnf. This seems more natural, even if it changes the strict meaning of hnf. This is source of incompatibilities as "intro" might succeed more often. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16338 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7