coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵	letouzey	2009-03-20
\| \| \| \| \| \|	user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleanup: remove unused config/giveostype.ml	letouzey	2009-03-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11973 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix de divers petits problèmes d'installation	notin	2009-02-11
\| \| \| \| \| \|	(cherry picked from commit 998a9a62874ba6cf26bdfe28f3ef0c72deaf0c25) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11918 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk	notin	2009-02-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11915 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add -coqtoolsbyteflags and -custom to ./configure...	glondu	2009-02-11
\| \| \| \| \| \|	...and use -custom by default on Windows and MacOS (backport r11895) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11913 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Conversion du fichier 'revision' en un fichier .ml + correction d'un bug ↵	notin	2009-01-06
\| \| \| \| \| \|	dans le configure introduit par les révisions 11754 et 11755 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11756 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Report de la révision 11754 (compilation sous windows)	notin	2009-01-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11755 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage des variables Coq et amélioration de coqmktop. Les	notin	2008-12-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	principaux changements sont: - coqtop (et coqc) maintenant insensible aux variables d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les librairies Coq peut être spécifié par l'option -coqlib - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les chemins des exécutables OCaml; en dehors du mode boot, coqmktop cherche les exécutables OCaml dans PATH - installation des .cmxs .o et .a en plus des .cm[ioxa]; ceux-ci étant installé en copiant l'architecture des sources (ie lib.cmxa est installé dans COQLIB/lib/lib.cmxa) - coq_makefile prend maintenant 3 paramètres sous forme de variables d'environnement: COQBIN pour dire où trouver les exécutables Coq, CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les chemins vers les librairies sont déduits en utilisant -where Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de simuler les conditions de la vie réelle (Ocaml pas dans le PATH, installation binaire relocalisée, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix CAMLHLIB (due to r11358) (Closes: #1986)	glondu	2008-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11532 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Native "Declare ML Module" when possible	glondu	2008-10-28
\| \| \| \| \| \| \| \| \|	Dynlink.add_{interfaces,available_units} are deprecated and not implemented natively. Currently, native "Declare ML Module" doesn't work because of this. Dynlink-related should be switched to the API introduced in OCaml 3.07. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11518 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Install dllcoqrun.so and use it by default	glondu	2008-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11371 85f007b7-540e-0410-9357-904b9bb8a0f7
*	$(COQLIB) -> $(COQLIBINSTALL) in Makefiles	glondu	2008-09-06
\| \| \| \| \| \| \|	COQLIB has a special meaning to executables, and we don't want make to set it to a path surrounded by double quotes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11367 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Parametrize link flags for VM-dependent bytecode	glondu	2008-09-05
\| \| \| \| \| \| \| \| \|	* Remove unneeded -custom flags. * Replace needed ones by a configure parameter. Setting it to "-dllib -lcoqrun" enables the creation/usage of pure bytecode executable provided the so/dll with the VM is found by ocamlrun. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11363 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Build coqrun library using ocamlmklib...	glondu	2008-09-05
\| \| \| \| \| \|	...instead of plain ar, so that .so (and .dll) is also created. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11362 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add -browser option to configure script	glondu	2008-07-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11271 85f007b7-540e-0410-9357-904b9bb8a0f7
*	moved magic numbers to configure (share coq/coqchk)	barras	2008-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11254 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'une option pour contrôler l'installation automatique de la ↵	notin	2008-07-16
\| \| \| \| \| \|	documentation + ajout d'un test pour hevea et latex git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11227 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix caml debug flags configuration, -g works with the native compiler only	msozeau	2008-05-19
\| \| \| \| \| \| \|	since 3.10. Fix a bug in classes when the instance database is empty. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10945 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Integration of theories/Ints into theories/Numbers, again : better ↵	letouzey	2008-05-08
\| \| \| \| \| \| \| \| \| \| \| \|	generation of NMake.v - genN.ml becomes NMake_gen.ml - no need to produce the corresponding binary: we use ocaml NMake_gen.ml > NMake.v - beware! redoing a ./configure is mandatory after this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10903 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plongement de doc/Makefile dans la nouvelle architecutre des Makefile	notin	2008-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10570 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration de la génération des graphes de dépendances	notin	2008-01-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10438 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option -lablgtkdir au configure (basé sur patch de Guillaume	herbelin	2007-10-04
\| \| \| \| \| \| \| \|	Rousse -- rapport de bug #1713) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10176 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compilation sous windows	notin	2007-10-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10171 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix a problem doing 'make clean' under Winodws	notin	2007-10-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10165 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
*	Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et ↵	herbelin	2007-08-24
\| \| \| \| \| \|	-rectypes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10091 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New bootstrapping, improved, Makefile system	corbinea	2007-07-13
\| \| \| \| \| \| \|	Documented in dev/doc/build-system.txt . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9992 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'une option -annotate au configure+ changement du comportement par ↵	notin	2006-10-11
\| \| \| \| \| \|	défaut de make git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9232 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compilation de Coq sous Windows	notin	2006-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9137 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite ajout option -ocamlib à configure	notin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9115 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification du configure pour paramétrer les exécutables liés à la ↵	notin	2006-08-30
\| \| \| \| \| \|	compilation C git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9099 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compilation de Coq sous Windows	notin	2006-08-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9098 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de l'appel aux exécutables Caml (noms absolus)	notin	2006-08-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9095 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modifications dans les scripts de configuration (coqtop et coqide affichent ↵	notin	2006-07-28
\| \| \| \| \| \|	maintenant le numéro de révision svn) + correction problème OCaml 3.07 et caml_;odify git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9063 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'une option -with-geoproof à la configuration et à l'exécution	notin	2006-06-09
\| \| \| \| \| \| \| \|	pour inhiber la gestion de Geoproof sous Coqide (qui peut poser des problèmes avec GTK < 2.6.0) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8932 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- intégration de la modification suggérée par L. Mamane: coqmktop passe ↵	notin	2006-05-04
\| \| \| \| \| \| \| \| \| \|	maintenant aussi l'option -dtypes à ocamlmktop - ajout d'une variable USERFLAGS, permettant à un utilisateur de rajouter facilement des options de compilation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8787 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite de l'ajout des FSets/FMaps dans les theories standards	letouzey	2006-04-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	-> OrderedTypeEx: des exemples de OrderedType -> OrderedTypeAlt: une definition alternative de OrderedType -> FSetAVL et FMapAVL: realisation a coup d'AVL -> FMapPositive: realisation a coup d'arbre binaire (selon les chiffres binaires de la cle) -> FMapIntMap : realisation en utilisant IntMap -> FSetToFiniteSet: un ensemble de FSet est un ensemble de Ensemble.v FSetAVL et FMapAVL prenent 30 secondes chacuns sur ma machine: on peut ne pas les compiler en passant l'option "-fsets no" a configure, de facon similaire a "-reals no" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8773 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵	notin	2006-04-28
\| \| \| \| \| \|	'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compatibilité ocaml 3.09	herbelin	2005-11-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7514 85f007b7-540e-0410-9357-904b9bb8a0f7
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place mécanisme de compatibilité ocaml 3.08	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5929 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
*	install de coqdoc	barras	2004-03-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5523 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqdoc	filliatr	2004-02-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5379 85f007b7-540e-0410-9357-904b9bb8a0f7
*	pour win32	coq	2004-01-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5270 85f007b7-540e-0410-9357-904b9bb8a0f7
*	configure et make install s'occupent de CoqIde tout seuls	filliatr	2003-05-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4029 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Option pour compiler une version 'light' des réels	desmettr	2002-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3299 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pour déterminer sous Windows si ocaml est en version cygwin ou win32	herbelin	2002-01-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2391 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ ocaml 3.04 sur Windows	herbelin	2002-01-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2387 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	courant	2001-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1612 85f007b7-540e-0410-9357-904b9bb8a0f7