aboutsummaryrefslogtreecommitdiff
path: root/scripts
AgeCommit message (Collapse)Author
2004-03-09option -l de coqc non reconnue (coq-bugs #509)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5443 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-26deplacement des cma et cmxa dans les sous-repertoiresbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5249 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-14make libraries, lexing of more utf8 symbolsmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5201 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-30option -strict-implicit pas reconnuebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5162 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-30ameliorations coqidecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5161 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-08Ajout option -impredicative-setherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4829 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Renommage no-strict en -strict-implicit; option -dont-load-proofsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4540 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Inclusion automatique de highparsingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4384 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Fusion -translate et -ftranslateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4276 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-04-09Coqide : introduction des coprocessus. CoqIde est maintenant interruptiblemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3887 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-08on repasse aussi -thread a Camlfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3872 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-17coqmktop: -ide fait ce qu'il faut (on peut maintenant construire des Coq IDE ↵filliatr
customises) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3778 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
2003-02-04interface GTK2 experimentalemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3660 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-04Contournement de ocamlmktop qui plante sous win32herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3657 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-14Réforme de l'interprétation des termes :herbelin
- 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
2002-11-05Intégration des modifs de la branche mowgli :herbelin
- 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
2002-09-17echappements incorrects dans chainefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3015 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@2734 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
2001-11-30Ajout d'un "\" pour proteger un autre "\" et ainsi etre compatible avecclrenard
ocaml 3.03 malgre un bug de lexing dans camlp4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2250 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-26Protection contre erreurs Unixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2072 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18Ajout d'une option et d'une fonction compile pour fabriquer les .voherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1984 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-17quotation des noms de fichiers pour eviter une mauvaise interpretation des \barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1974 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Amélioration check_module_nameherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1939 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20support option -R pour coqdepfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1640 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-21option -verbose a coqc; option -i suppriméefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1474 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-03-15les options passées sont prioritaires sur les -I par défautfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1468 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-06modifs pour extraction; bug coqmktopfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1428 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-28bug Reset et Sectionsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1410 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-09option -m (utilisation memoire)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1366 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-01- coqc : option -imagefilliatr
- coqmktop : manquaient des -I - tauto : rétablissement du vieux tauto en attendant la stabilité du nouveau - correction d'un bug de Simpl avec Fix (découvert dans preuve FTA) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1304 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Suppresion de l'option -as, c'est maintenant -R qui devient l'option ↵herbelin
standard pour associer un nom physique à un nom logique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1066 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-30Changement de la syntaxe des options -I et -Rherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1038 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-03Deplacement d'options avec ou sans argtsmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@799 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-03compilation des fichiers ml4 sans GNUseriesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@795 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-31- simplification Makefile (compilation des fichiers .ml'; pas encore parfaitfilliatr
car on passe par les fichiers .ml) - Require Export enfin rétabli avec la bonne sémantique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@792 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27g_natsyntax et g_zsyntax maintenant toujours linkesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@773 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Capture erreur de create_processherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@536 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-08contrib linkees en natiffilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@431 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05Ajoute option -byteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@420 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
2000-04-28portage en ocaml / camlp4 3.00filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@379 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 20:03:07 +0000