coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	BIG MAJ Extraction:	letouzey	2003-04-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	------------------ - (Recursive) Extraction Module devient (Recursive) Extraction Library (pour cause d'ambiguite avec les nouveaux modules Coq). - un nouveau Extraction Module qui extrait dans le toplevel tout module Coq - tout fixpoint est de nouveau inlinable (Yves). - fix bug du calcul d'env minimal des modules en extraction monolithique. - un nouveau fichier Modutil regroupant manques de Modops & functions specifiques aux modules MiniML - plus d'aliases a trainer (mais des substitutions des le depart) - ET SURTOUT: un nommage correct (ou du moins moins pire) dans les modtypes et les functors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3934 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction des modules, enfin !	letouzey	2003-01-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3569 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug pp letin + un inductif constant n'est pas un record	letouzey	2002-11-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3324 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj avec tous les mli	letouzey	2002-11-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3207 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un fichier a utiliser via Drop pour le debug de l'extraction.	letouzey	2002-11-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3206 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
*	maj test des reals	letouzey	2002-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2636 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ↵	letouzey	2002-04-08
\| \| \| \| \| \|	dummy git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2619 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise jour	filliatr	2002-04-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2613 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
*	reparation du test des reals	letouzey	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2561 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deux fichiers supplementaires de customisation d'extraction	letouzey	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2557 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement du test extraction suite aux modif inining	letouzey	2002-03-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2556 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Big commit extraction:	letouzey	2002-03-04
\| \| \| \| \| \| \| \| \| \| \|	- Changement de syntaxe (Extraction Language Toplevel/Ocaml/Haskell) - Retour des inductifs singletons et vides dans extraction.ml (extraction.ml -> actions sur le type, mlutil.ml -> conserve le type) - maintenant par defaut Recursive Extraction === Extraction "file" - kill_prop global est fait dans extraction.ml selon typage (a suivre...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2508 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite et fin (?) de haskell: gestion des modules, mise en place du'un test	letouzey	2002-02-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2480 85f007b7-540e-0410-9357-904b9bb8a0f7
*	qq inline manuels (sigS_rec ...) + utilisation de library_part	letouzey	2002-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2476 85f007b7-540e-0410-9357-904b9bb8a0f7
*	gros changement dans mlutil.ml: ajout d'une elimination globale des prop	letouzey	2002-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2456 85f007b7-540e-0410-9357-904b9bb8a0f7
*	adaptation de l'extraction aux changements de Christine concernant rec/rect ↵	letouzey	2002-01-31
\| \| \| \| \| \|	et False_rec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2448 85f007b7-540e-0410-9357-904b9bb8a0f7
*	debranchement du test sur les Reals	letouzey	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2344 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction de bugs concernant la gestion des modules. debranchement du test ↵	letouzey	2001-12-10
\| \| \| \| \| \|	d'extraction sur les Reals en attendant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2282 85f007b7-540e-0410-9357-904b9bb8a0f7
*	remise au gout du jour du repertoire theories/Sorting de la V6.3	letouzey	2001-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2231 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moins de fichiers avec des axioms	letouzey	2001-11-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2188 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Refonte du fichier mlutil.ml. Correction d'un bug d'optim case	letouzey	2001-11-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2167 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite des tests	letouzey	2001-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2166 85f007b7-540e-0410-9357-904b9bb8a0f7
*	refonte du test	letouzey	2001-11-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2162 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement epsilonesque	letouzey	2001-11-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2155 85f007b7-540e-0410-9357-904b9bb8a0f7
*	retablissement de l'optim case constant	letouzey	2001-11-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2154 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout du script qualify2open qui met des open Truc en debut de fichier	letouzey	2001-11-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2153 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ↵	letouzey	2001-10-26
\| \| \| \| \| \|	ETC etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2141 85f007b7-540e-0410-9357-904b9bb8a0f7
*	chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les ↵	letouzey	2001-10-22
\| \| \| \| \| \|	options git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2133 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changements mineurs du test	letouzey	2001-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2020 85f007b7-540e-0410-9357-904b9bb8a0f7
*	adaptation a la nouvelle syntaxe Extract Inlined Constant	letouzey	2001-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2001 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement du make depend en vu du make reals	letouzey	2001-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1948 85f007b7-540e-0410-9357-904b9bb8a0f7
*	2 bugs: typevarlist pour inductifs + args pour flexibles	letouzey	2001-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1800 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise en place extraction haskell	filliatr	2001-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1751 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nettoyage extraction	filliatr	2001-05-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1737 85f007b7-540e-0410-9357-904b9bb8a0f7
*	make reals prend en compte tous les .vo de theories/Reals	filliatr	2001-04-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1712 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
*	Ajout du .depend	mohring	2001-04-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1693 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retire theories/Num	mohring	2001-04-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1692 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fin d'optimisation (cas modules) + warning pour coind & ocaml	letouzey	2001-04-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1685 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour	letouzey	2001-04-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1671 85f007b7-540e-0410-9357-904b9bb8a0f7
*	realisation des reals	letouzey	2001-04-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1670 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remaniement Makefile de test. make reals possible	letouzey	2001-04-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1661 85f007b7-540e-0410-9357-904b9bb8a0f7
*	scripts; extraction False_rec	filliatr	2001-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1635 85f007b7-540e-0410-9357-904b9bb8a0f7
*	blindage False_rec	filliatr	2001-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1634 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modifs des scripts de test auto	filliatr	2001-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1621 85f007b7-540e-0410-9357-904b9bb8a0f7
*	script de bench automatique pour extraction	letouzey	2001-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1615 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