aboutsummaryrefslogtreecommitdiff
path: root/config
AgeCommit message (Collapse)Author
2006-08-29Compilation de Coq sous Windowsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9098 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-29Changement de l'appel aux exécutables Caml (noms absolus)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9095 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-28Modifications dans les scripts de configuration (coqtop et coqide affichent ↵notin
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
2006-06-09Ajout d'une option -with-geoproof à la configuration et à l'exécutionnotin
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
2006-05-04- intégration de la modification suggérée par L. Mamane: coqmktop passe ↵notin
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
2006-04-29suite de l'ajout des FSets/FMaps dans les theories standardsletouzey
-> 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
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵notin
'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-04Compatibilité ocaml 3.09herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7514 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Mise en place mécanisme de compatibilité ocaml 3.08herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5929 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17install de coqdocbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5523 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-24coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5379 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29pour win32coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5270 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19configure et make install s'occupent de CoqIde tout seulsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4029 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Option pour compiler une version 'light' des réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3299 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-11Pour déterminer sous Windows si ocaml est en version cygwin ou win32herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2391 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-10MAJ ocaml 3.04 sur Windowsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2387 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19*** empty log message ***courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1612 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24- coqc: utilise le meilleur coq possiblefilliatr
- coqc -v réparé - coqtop: options -byte et -opt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@940 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-11Prise en compte camlp4.opt dans la configuration et le Makefileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@844 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08nouveau load pathfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@828 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-27Retrait du 'strip' en cas de profilingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@518 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03compilation bytecode / native :filliatr
- script de configuration - Makefile - simplification de coqmktop - option -opt de coqc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@413 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-11mise en place des outilsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@236 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-10 - erreurs Pretypefilliatr
- Write / Restore State git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@230 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-08-19mise en place programmation literaire (generation de doc/coq.tex)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-08-16Initial revisionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 16:27:37 +0000