coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	mdule --> module	mohring	2002-12-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3374 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fichiers DOS	filliatr	2002-12-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3371 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug de coqdep qui n'acceptait pas les fichiers DOS (cf Binome.v)	letouzey	2002-11-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3243 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bugs	herbelin	2002-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3236 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
\| \| \| \| \| \| \| \| \| \| \|	- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
*	commit du calcul des dependances un peu plus robuste	barras	2002-10-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3147 85f007b7-540e-0410-9357-904b9bb8a0f7
*	gestion coherente de l'option -R et des Require A.B.C.	barras	2002-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3112 85f007b7-540e-0410-9357-904b9bb8a0f7
*	backslahs foireux	filliatr	2002-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3059 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Filtrage redondant	herbelin	2002-09-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3042 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un peu plus de flexibilité pour la position du '.' final	herbelin	2002-09-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3010 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile utilise maintenant coqdoc	filliatr	2002-06-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2793 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout des -I contrib	herbelin	2002-05-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2738 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵	herbelin	2002-05-29
\| \| \| \| \| \|	commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq-inferior, by Marco Maggesi	filliatr	2002-04-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2644 85f007b7-540e-0410-9357-904b9bb8a0f7
*	meilleure gestion du point terminal	filliatr	2002-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2611 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bootstrap consistent avec les options de la ligne de commande	filliatr	2002-02-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2478 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation du make depend et du .depend	letouzey	2001-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Encapsulage des '<' et '>' pour éviter le regroupement '«'	herbelin	2001-10-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2092 85f007b7-540e-0410-9357-904b9bb8a0f7
*	la cible all était incomplète	filliatr	2001-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2003 85f007b7-540e-0410-9357-904b9bb8a0f7
*	make install dans coq_makefile et repertoire associe user-contrib ajoute au ↵	filliatr	2001-09-19
\| \| \| \| \| \|	load path au demarrage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1999 85f007b7-540e-0410-9357-904b9bb8a0f7
*	prise en compte de Load par coqdep	filliatr	2001-08-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1918 85f007b7-540e-0410-9357-904b9bb8a0f7
*	"make clean" nettoie les .g all.ps all-gal.ps et les fichiers HTML	filliatr	2001-07-17
\| \| \| \| \| \| \|	générés à partir des .v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1856 85f007b7-540e-0410-9357-904b9bb8a0f7
*	all.g.ps -> all-gal.ps	filliatr	2001-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1855 85f007b7-540e-0410-9357-904b9bb8a0f7
*	compat -sort et -suffix	filliatr	2001-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1854 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cibles all.ps et all-gal.ps (utilisation de coqweb)	filliatr	2001-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1853 85f007b7-540e-0410-9357-904b9bb8a0f7
*	utilisation de printf (simplif)	filliatr	2001-07-16
\| \| \| \| \| \| \|	option -sort pour trier les .v selon les dépendances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1852 85f007b7-540e-0410-9357-904b9bb8a0f7
*	plus besoin de separer les ?	barras	2001-06-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1786 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Chgt de MAKE= ...	letouzey	2001-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1771 85f007b7-540e-0410-9357-904b9bb8a0f7
*	option -byte	filliatr	2001-05-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1769 85f007b7-540e-0410-9357-904b9bb8a0f7
*	application patch Claudio	filliatr	2001-05-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1746 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Ajout pages de man pour coqc, coqtop, coqtop.opt et coqtop.byte	courant	2001-04-25
\| \| \| \| \| \| \| \| \|	- Deplacement pages de tools/ vers man/ - Modif distrib/Makefile pour Debian - Modif mode emacs pour Debian git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1710 85f007b7-540e-0410-9357-904b9bb8a0f7
*	patch Claudio pour coq_makefile	filliatr	2001-04-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1660 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Hints.... added next to Hint....	coq	2001-04-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1646 85f007b7-540e-0410-9357-904b9bb8a0f7
*	support option -R pour coqdep	filliatr	2001-04-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1640 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	courant	2001-04-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1598 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug Print Proof; usage coqtop/coqc	filliatr	2001-04-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1552 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout de coq_example# dans coq-tex	werner	2001-04-04
\| \| \| \| \| \| \|	BW git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1548 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
*	modifs mineures	filliatr	2001-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1354 85f007b7-540e-0410-9357-904b9bb8a0f7
*	backtrack sur le lexeur de la V6	filliatr	2001-01-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1289 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des ??	herbelin	2001-01-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1234 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2000-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1223 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traducteur automatique de scripts vernac	herbelin	2000-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1198 85f007b7-540e-0410-9357-904b9bb8a0f7
*	numarg -> pure_numarg a poursuivre	mohring	2000-12-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1084 85f007b7-540e-0410-9357-904b9bb8a0f7
*	do_Makefile -> coq_makefile pour le bootstrap!	filliatr	2000-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@835 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouveau load path	filliatr	2000-11-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@828 85f007b7-540e-0410-9357-904b9bb8a0f7
*	outils (manquent encore les deux filtres)	filliatr	1999-12-11
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@235 85f007b7-540e-0410-9357-904b9bb8a0f7