coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	chamboulement du codage des indcutifs extraits; deplacements des tables; ...	letouzey	2002-12-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3388 85f007b7-540e-0410-9357-904b9bb8a0f7
*	remaniement de test_extraction.v	letouzey	2002-11-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3256 85f007b7-540e-0410-9357-904b9bb8a0f7
*	L'extraction c'est magic cvs -n up	letouzey	2002-10-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3199 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	letouzey	2002-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2890 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Gros Remaniement Extraction:	letouzey	2002-07-16
\| \| \| \| \| \| \| \| \|	* extraction.ml + modulaire (cf extract_type) et + proche theorie (cf feu extract_app) * table.ml filtre les Extract Constant vers types ou terms * extract_env.ml refuse maintenant les Extraction constr. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2886 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation du cas des arguments de type qui sont des arités + patch dummy ↵	letouzey	2002-03-28
\| \| \| \| \| \|	applied git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2574 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Refonte complete de la génération des types ML	letouzey	2002-03-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2568 85f007b7-540e-0410-9357-904b9bb8a0f7
*	considerations de pretty-print	letouzey	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2558 85f007b7-540e-0410-9357-904b9bb8a0f7
*	gros commit: principalement ajout des lambdas arity + leur optimisation en ↵	letouzey	2002-03-15
\| \| \| \| \| \|	temps normal + beaucoup de simplifications diverses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2532 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cas des constructeurs singletons. Messages d'erreur. Revision de ↵	letouzey	2002-03-05
\| \| \| \| \| \|	test_extraction.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2514 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction du eta_expanse	letouzey	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2028 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite du musée des horreurs	letouzey	2001-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1759 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug cast	letouzey	2001-05-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1745 85f007b7-540e-0410-9357-904b9bb8a0f7
*	exemples Magic	letouzey	2001-05-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1742 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug dans eta-expansion des constructeurs. Argument Prop dans extract_type_app	letouzey	2001-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1575 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement type_var et signature	filliatr	2001-03-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1498 85f007b7-540e-0410-9357-904b9bb8a0f7
*	conservation des arguments dans Prop (snif)	filliatr	2001-03-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1495 85f007b7-540e-0410-9357-904b9bb8a0f7
*	trace des inductifs sur Prop	letouzey	2001-03-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1492 85f007b7-540e-0410-9357-904b9bb8a0f7
*	eta-expansion des constructeurs si necessaire (a posteriori en miniML)	filliatr	2001-03-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1481 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression des param dans inductifs. suite du Cases	letouzey	2001-03-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1479 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reecriture du extract_type pour Prod et Lambda. Eta-expansion dans les ↵	letouzey	2001-03-21
\| \| \| \| \| \|	branches des Cases (cf sumbool_rec) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1475 85f007b7-540e-0410-9357-904b9bb8a0f7
*	extraction naive de fix et case	filliatr	2001-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1471 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extract_term_with_type. mise a jour & verification des commentaires	letouzey	2001-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1470 85f007b7-540e-0410-9357-904b9bb8a0f7
*	entetes	filliatr	2001-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	interface du extract_rec. Extract_constr prend un environnement	letouzey	2001-03-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1464 85f007b7-540e-0410-9357-904b9bb8a0f7
*	signatures dans le bon ordre	filliatr	2001-03-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1459 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Finite	filliatr	2001-03-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification: plus de contexte pour extract_type et contexte simplifié ↵	filliatr	2001-03-13
\| \| \| \| \| \|	pour extract_term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1457 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite de la verification des assert false	letouzey	2001-03-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1456 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour commentaires'	filliatr	2001-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1449 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Commentaires. Verification des assert false. Probleme des types ML arity.	letouzey	2001-03-12
\| \| \| \| \| \| \|	Correction des dependances pour bin/coq-extraction dans le Makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1448 85f007b7-540e-0410-9357-904b9bb8a0f7
*	distinction contexte et signature	filliatr	2001-03-07
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1435 85f007b7-540e-0410-9357-904b9bb8a0f7