coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Prise en compte des dépendances des .ml	notin	2008-03-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10719 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New option -glob for coqdep, in order to avoid nasty tricks with sed in Makefile	letouzey	2008-03-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10668 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile : backtrack sur les liens vers les exécutables ocaml	notin	2008-03-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10638 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug de coq_makefile	notin	2008-03-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10633 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: correction de l'appel aux exécutables Ocaml	notin	2008-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10606 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: Correction d'un bug sur les options passées à Coqdoc	notin	2008-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10604 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Génération d'une toc en html et avec l'option -ps	notin	2008-02-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10597 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile: variables	notin	2008-02-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10586 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile: dépendances + génération des fichiers html	notin	2008-02-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10585 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petite correction sur coq_makefile	notin	2007-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10391 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des .glob par coq_makefile	notin	2007-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10231 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey	2007-09-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	the patch by S. Mimram) * for detecting architecture, also look for /bin/uname * restore the compatibility of kernel/byterun/coq_interp.c with ocaml 3.07 (caml_modify vs. modify). There is still an issue with this 3.07 and 64-bits architecture (see coqdev and a future bug report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- MAJ entêtes des fichiers produits par coq_makefile	herbelin	2007-05-16
\| \| \| \| \| \| \| \|	- Correction de bugs dans la reconnaissance d'un "*)" potentiel dans les lignes correspondant au mécanisme "section" de coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9826 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Améliorations utiles pour les Makefile répartis sur plusieurs répertoires	herbelin	2007-02-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	coqdep : - fonction de "canonisation" du nom des cibles plus performante (elle traverse notamment les "..") coq_makefile : - ajout automatique de "-I ." dans COQLIBS seulement si pas déjà déclaré (utile pour éviter les cibles en double dans coqdep en présence de -R) - explicitation de "-byte" dans la cible "byte:" (son absence semble remonter à l'époque où l'exécution en byte était le défaut) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9676 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification de l'appel à coqdoc (COQBIN)	notin	2006-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8840 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de l'essai d'effacement des noms des cibles custom par la cible clean	herbelin	2006-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7994 85f007b7-540e-0410-9357-904b9bb8a0f7
*	This commit corrects the last commit of Hugo that broke down the "make depend"	sacerdot	2005-01-12
\| \| \| \| \| \| \|	command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6578 85f007b7-540e-0410-9357-904b9bb8a0f7
*	VOFILES aussi pour make depend	herbelin	2004-12-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6444 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pour ceux qui appelent Makefile avec des fichiers dans des sous-répertoires	herbelin	2004-11-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6365 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	"xml" target removed from generated makefiles (since it was no longer used)	sacerdot	2004-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5602 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	kirchner	2004-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5601 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option -impredicative-set	herbelin	2003-11-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4829 85f007b7-540e-0410-9357-904b9bb8a0f7
*	rm -f .depend (sans le -f "make depend" echoue lorsque le .depend	filliatr	2003-07-02
\| \| \| \| \| \| \|	n'existe pas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4213 85f007b7-540e-0410-9357-904b9bb8a0f7
*	on sait se refaire uniquement si option -f	filliatr	2003-02-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3697 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile dit comment faire le .depend (evite l'echec lorsque	filliatr	2003-02-24
\| \| \| \| \| \| \|	.depend n'existe pas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3696 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
*	Filtrage redondant	herbelin	2002-09-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3042 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
*	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