coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	TODO	letouzey	2003-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4857 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj status de l'extraction des modules	letouzey	2003-02-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3649 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj V7.4	letouzey	2003-01-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3599 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	letouzey	2002-04-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2657 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj doc extraction dans repertoire contrib/extraction	letouzey	2002-04-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2643 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un peu de mise a jour de la doc extraction	letouzey	2002-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2535 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	letouzey	2001-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1760 85f007b7-540e-0410-9357-904b9bb8a0f7
*	TODO in v.o., test/Makefile moins pire, README avec ref	letouzey	2001-04-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1694 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uncurryfy_ast inutile depuis l'eta-expansion dans extraction.ml.	letouzey	2001-04-23
\| \| \| \| \| \| \| \| \| \| \| \|	Du coup MLcons avec 2 args seulement. Ne reclame pas de realiser axioms sur Prop. Optimizations=true par default pour Extraction Module. Simplifications naives des letin. Merge_app avant normalisation. Booleen expansion_test pour l'optimisation, avec test de strictness. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1662 85f007b7-540e-0410-9357-904b9bb8a0f7
*	synchonization des tables d'extraction	filliatr	2001-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1626 85f007b7-540e-0410-9357-904b9bb8a0f7
*	eliminiation des singletons du genre sig + divers	letouzey	2001-04-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1587 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug lift dans IsRel de extract_type. Axiomes dans extract_type	letouzey	2001-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1570 85f007b7-540e-0410-9357-904b9bb8a0f7
*	axiomes dans les types	filliatr	2001-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1549 85f007b7-540e-0410-9357-904b9bb8a0f7
*	rollback sur les commandes Extract Constant/Inductive; nettoyage et ↵	filliatr	2001-04-04
\| \| \| \| \| \|	documentation code git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1528 85f007b7-540e-0410-9357-904b9bb8a0f7
*	commandes Extract Constant/Inductive; message d'erreur pour les axiomes	filliatr	2001-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1526 85f007b7-540e-0410-9357-904b9bb8a0f7
*	inductifs vides	filliatr	2001-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1513 85f007b7-540e-0410-9357-904b9bb8a0f7
*	à faire	filliatr	2001-04-02
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1511 85f007b7-540e-0410-9357-904b9bb8a0f7