coq - The formal proof system

Age	Commit message (Collapse)	Author
2008-05-22	QRewrite is now obsolete. It was containing manual ltac stuff	letouzey
	for helping rewriting under Quantifiers and binders, but Matthieu's setoid rewrite now has the same kind of capabilities by default. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10966 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-15	Coq headers + $ in theories/Numbers files	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10934 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-07	Replaced BinNat with a new version that is based on ↵	emakarov
	theories/Numbers/Natural/Binary/NBinDefs. Most of the entities in the new BinNat are notations for the development in Numbers. Also added min and max to the new natural numbers and integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10298 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-03	An update of theories/Numbers	emakarov
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10285 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-01	Added the compilation of theories/Numbers to Makefile.common. The following ↵	emakarov
	things compile: abstract natural numbers and integers with plus, times, minus, and order; Peano and binary implementations for natural numbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10161 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-13	Update before joining all signatures into one.	emakarov
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10119 85f007b7-540e-0410-9357-904b9bb8a0f7