coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	typo	marche	2003-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8387 85f007b7-540e-0410-9357-904b9bb8a0f7
*	relecture JCF	filliatr	2003-12-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8374 85f007b7-540e-0410-9357-904b9bb8a0f7
*	added Firstordre and Congruence	corbinea	2003-12-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8372 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Label redondant	herbelin	2003-11-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8364 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a tactic entry for Jprover + commented out inputenc in the main file	corbinea	2003-10-30
\| \| \| \| \| \| \|	(no use having both fontenc and inputenc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8347 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ Double Inductive vis a vis de la V7.4	herbelin	2003-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8346 85f007b7-540e-0410-9357-904b9bb8a0f7
*	passage V8	filliatr	2003-09-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8341 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added the documentation on Functional Scheme (a command, I also put	courtieu	2003-06-21
\| \| \| \| \| \| \| \|	some examples in RefMan-tacex.tex) and Functional Induction (a tactic). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8335 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout 'in (Type of ...)'	herbelin	2003-05-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8334 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ Simpl et Change	herbelin	2003-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8331 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction typo d'un but Tauto	herbelin	2002-09-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8293 85f007b7-540e-0410-9357-904b9bb8a0f7
*	documentation variante Subst (sans argument)	filliatr	2002-09-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8292 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Subst	filliatr	2002-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8291 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ syntaxe 'Hint Rewrite'	herbelin	2002-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8289 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ V7.3	herbelin	2002-05-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8280 85f007b7-540e-0410-9357-904b9bb8a0f7
*	doc Intuition et Tauto	courant	2002-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8277 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout Rename et Pose	herbelin	2002-04-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8276 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Quelques pr�cisions sur la convertibilit� et les tactiques Cbv/Lazy	herbelin	2002-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8273 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout ClearBody et Assert H:=t	herbelin	2001-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8260 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout fonctionnalit� Intros Until de Injection, Discriminate et Simplify_eq	herbelin	2001-10-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8245 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding documentation for a variant of Inversion, where a numeric argument,	bertot	2001-10-09
\| \| \| \| \| \| \| \|	referring to the nth non-dependent product in the goal's conclusion, can be given instead of an hypothesis name. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8244 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ Intro + divers	herbelin	2001-10-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8239 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Diverses MAJ V7.1 autour des qualid	herbelin	2001-09-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8221 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation NewInduction, NewDestruct, LetTac, Assert	herbelin	2001-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8217 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fourier, Reals,...	mayero	2001-04-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8201 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'une ref pour Field	delahaye	2001-04-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8197 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de Field	delahaye	2001-04-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8196 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de Zarith en ZArith	mohring	2001-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8194 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intros Pattern wildcard	mohring	2001-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8189 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ decompose	herbelin	2001-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8182 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revision Tauto, AutoRewrite + Ajout de Ltac	delahaye	2001-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8172 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour V7	filliatr	2001-04-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8171 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour V7	filliatr	2001-04-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8169 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Initial revision	filliatr	2000-12-12
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8143 85f007b7-540e-0410-9357-904b9bb8a0f7