coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Renommage AppL en App	herbelin	2000-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@635 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Disparition du type oper mais nouveau type global_reference	herbelin	2000-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@620 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abstraction de constr	herbelin	2000-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin	2000-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de Abst	herbelin	2000-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un LetIn primitif.	herbelin	2000-09-10
\| \| \| \| \| \| \|	Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
*	) -> i)	filliatr	2000-07-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@566 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Opaque pas encore implementee; syntax langage tactiques	filliatr	2000-07-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@552 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- $BINDER -> BINDER dans g_constr.ml4 (=> erreur syntax Fix)	filliatr	2000-06-21
\| \| \| \| \| \| \|	- suite portage Ring git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@516 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> ↵	filliatr	2000-06-21
\| \| \| \| \| \|	.vo plus petits git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@514 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ring	filliatr	2000-06-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@512 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Auto with zarith provisoirement remplace par un Omega	filliatr	2000-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@506 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un Declare ML Module inutile	filliatr	2000-05-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@430 85f007b7-540e-0410-9357-904b9bb8a0f7
*	retour a la version qui ne contournait pas le bug de PatternMatchingFailure ↵	herbelin	2000-05-03
\| \| \| \| \| \|	non trappe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@406 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du langage de tactiques	delahaye	2000-05-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
*	portage Omega (mais toujours pas Zpower et Zlogarithm)	filliatr	2000-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@400 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MODIFS pour compatibilité aussi 2.99	herbelin	2000-04-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@391 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise sous CVS d'Omega	filliatr	2000-04-28
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@380 85f007b7-540e-0410-9357-904b9bb8a0f7