aboutsummaryrefslogtreecommitdiff
path: root/lib/options.ml
AgeCommit message (Collapse)Author
2003-09-22Passage à la V8 par défautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4437 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et ↵herbelin
choix du parseur en fonction de cette option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4387 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Positionnement precoce de l'option -v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4270 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Option -v8 à coqtop lance coqtopnew; option -no-strict; option -no-proofsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4254 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-12Ajout option translate_syntax pour caractériser l'interprétation du ↵herbelin
traducteur à proprement parler git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4139 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Mise en place d'un 2ème traducteur à l'essai (activable avec -ftranslate2)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3981 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-01Déplacement with_option dans Optionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3835 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-05Ajout du traducteurdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3664 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-10Ajout options -v7 et -v8, et commandes V7only et V8onlyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3407 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05Nouvelle option -xml à coqtop pour compiler un développement enherbelin
l'exportant au format xml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3211 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14option -dump-glob pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18Le chargement des coercions est nécessaire même si le module n'est pas ouvertherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2409 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-28option -qualityfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1767 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-04-03utilisation de Options.if_verbosefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1519 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
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en ↵herbelin
compte des défs locales dans les arguments des inductifs; nettoyage divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1388 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-12modules et coqcfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@239 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-09Discharge (encore bugge)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@223 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01poursuite de Vernacentriesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@178 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-26module Classops; ajout de fonctions dans Declare en consequencefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@152 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-26ajouts divers pour module Printerfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@145 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-28ajout de divers fonctions dans lib/filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@82 85f007b7-540e-0410-9357-904b9bb8a0f7