coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	More OCaml-3.11-friendly configure script	glondu	2008-10-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11487 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
*	Create the bin/ directory if non-existent	glondu	2008-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11369 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Always use environment variables	glondu	2008-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11368 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
*	Revert commit 11326, to see if it is what makes bench fail	glondu	2008-08-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11329 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mind environment variables in (generated) coq_config.ml	glondu	2008-08-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11326 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
*	Detection de l'architecture sous Windows (et sans uname -o)	notin	2008-06-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11137 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Où l'on se débarrasse de uname -o	notin	2008-06-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11135 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compilation Windows	notin	2008-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11113 85f007b7-540e-0410-9357-904b9bb8a0f7
*	2-3 petites modifs sur la doc	notin	2008-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11091 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement des echo -e par printf + bug sur les exécutables ocaml dans ↵	notin	2008-06-09
\| \| \| \| \| \|	coq_makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11079 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petites corrections diverses :	herbelin	2008-06-02
\| \| \| \| \| \| \| \| \| \| \|	- bug d'installation (coq_config.cmo était installé une 2ème fois au lieu d'installer coq_config.cmx) - suite nettoyage configure, option reals - ajout d'une option "only parsing" oubliée dans Peano.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11035 85f007b7-540e-0410-9357-904b9bb8a0f7
*	On cesse de demander une valeur pour l'option reals si l'utilisateur	herbelin	2008-06-01
\| \| \| \| \| \| \| \| \| \|	n'en donne pas (ça paraît plus simple vu que le temps de compil de reals est devenu mineur, et on fait comme pour fsets qui par défaut est compilé). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11031 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Quelques amendements liées à la compilation des packages.	herbelin	2008-06-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- typo du configure; - warnings variables non utilisées dans ide/utils; - suppression des variables vides COQINSTALLPREFIX et OLDROOT parce que l'option -e que l'on aurait pu en principe utiliser pour les surcharger ne fonctionne pas lorsqu'il y a plusieurs niveaux d'imbrication de makefiles (comme c'est le cas quand on vient du makefile servant à faire les packages qui appelle le makefile principal qui appelle les makefile.stage); - utilisation de ALLVO plutôt qu'un find pour trouver les .v sur lesquels appliquer coqdep (permet d'éviter des warning sur les fichiers de test, non prévus pour faire partie de la biblio standard); - utilisation de -custom sur les bytecode qui ne l'étaient pas encore (coqchk et coqmktop) pour être indépendant de ocamlrun à l'installation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11029 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
*	Fix a de Bruijn bug in setoid_rewrite when rewriting under	msozeau	2008-05-17
\| \| \| \| \| \| \| \| \| \|	a non-dependent product under a lambda. Now qiff can be replaced by a simple setoid_rewrite in NumPrelude. Change configure to not do stripping if compiling with -g... Add -g / CAMLDEBUG flags to the native compilation command too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10941 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
*	Test pour compilation native camlp5	herbelin	2008-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10818 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test make 3.81	herbelin	2008-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10754 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Correction d'un bug de coq_makefile sur les variables CAMLLIBS et	notin	2008-04-03
\| \| \| \| \| \| \| \| \| \|	COQLIBS. - Ajout d'un message d'erreur si Camlp5 est compilé en mode strict git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10746 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
*	Résolution d'une confusion dans le rôle des variables CAMLP4 et CAMLP4LIB:	herbelin	2008-02-06
\| \| \| \| \| \| \| \|	- CAMLP4 dit si on utilise camlp4 ou camlp5 - CAMLP4LIB est le chemin camlp4/5 à donner en option -I git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10517 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection contre l'erreur mentionnée dans le rapport de bug 1790	herbelin	2008-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10513 85f007b7-540e-0410-9357-904b9bb8a0f7
*	migration of ide/utf8.v to theories/Unicode/Utf8.v	letouzey	2007-12-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	These notations aren't CoqIDE-specific, I can now use them with ProofGeneral (after a small modification of PG, contact me if you're interested by the patch). So let's place this file in a globally visible subdir of theories/. By the way, the filename is now uppercase as all other .v files. By the way, minor other changes in Makefile : extraction/test doesn't exist anymore, and tags / otags can be made without re-doing any find. NB: be sure to use etags that comes from emacs and not the one of exuberant-ctags, since the latter has now a different syntax (in debian, see update-alternatives etags). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10376 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added transitivity and irreflexivity of <, as well as < -elimination for ↵	emakarov	2007-10-16
\| \| \| \| \| \| \| \| \|	binary positive numbers. Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10226 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug variable CAMLP4 qui ne doit pas contenir un chemin mais le type de ↵	herbelin	2007-10-11
\| \| \| \| \| \|	preprocesseur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10214 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Verification ocaml >= 3.09.3 pour coq natif sous MacOS X Pentium	herbelin	2007-10-09
\| \| \| \| \| \| \|	+ uniformisations des messages utilisateurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10203 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Détection de camlp5 5.00 au configure	herbelin	2007-10-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10190 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de la possibilité de donner le chemin de la bibliothèque camlp5	herbelin	2007-10-07
\| \| \| \| \| \| \|	+ recherche par défaut de camlp5 et lablgtk aussi dans site-lib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10189 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petite reparation de la config pour camlp5 apres le commit 10164	letouzey	2007-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10181 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
*	Report des modifications faites sur le configure en r10039, r10052, r10053 ↵	notin	2007-10-02
\| \| \| \| \| \|	et r10054 dans les branches trunk et v8.1 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10164 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
*	Modification de l'initialisation des chemins de la librairie standard	notin	2007-08-20
\| \| \| \| \| \| \| \| \|	pour imposer un ordre précis des répertoires (résout en partie le problème entre Init.Wf et Program.Wf.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10081 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
*	Le configure et le README accordent leurs violons pour exiger ocaml 3.07 ↵	herbelin	2007-04-24
\| \| \| \| \| \|	(restera à accorder les .spec) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9792 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revision of the coqide configuration:	letouzey	2007-02-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* if -byte-only is used, then -coqide byte is implied except when the user explicitely said otherwise * If the user asks -coqide opt or byte, then LablGtk2 checks are not bypassed anymore. In particular, the check whether ide/undo.mli should be compatible with LablGtk2 < 2.6.0 or >= 2.6.0 is done. * The tests are organized in a linear sequence of "if elif elif else" that the next reader of this code may have a chance to understand git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9681 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Merge from Lionel Elie Mamane's private branch:	lmamane	2007-01-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Makefile: Option (environment variable NO_RECOMPILE_LIB) to not recompile the whole standard library just because the coq binaries got rebuilt. - Infrastructure to change the object pretty-printers at runtime. - Use that infrastructure to make coqtop-protocol with Pcoq trees and Pcoq-protocol with pretty-printed terms possible in coq-interface. - Make "Back(track)" into closed sections, modules and module types "Just Work™". - Modernise/generalise Pcoq protocol a bit, make some of its warts optional. - Implement "Show." in Pcoq mode. - Add Rpow_def.vo to REALSBASEVO so that its dependencies are computed (and used). - "make revision" now handles GNU Arch / tla in addition to svn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9476 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adaptation à FreeBSD	notin	2006-11-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9378 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement du magic number	notin	2006-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9346 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de la valeur par défaut de with_geoproof (stabilité coqide)	notin	2006-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9271 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
*	Bug dans configure (test best_compiler)	notin	2006-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9139 85f007b7-540e-0410-9357-904b9bb8a0f7