aboutsummaryrefslogtreecommitdiff
path: root/scripts/coqc.ml
AgeCommit message (Collapse)Author
2010-09-14CoqIDE argv parsing delegated to coqtopvgross
Introduces some hacks to have a consistent user experience. When coqtop prints info on self then exit, return code is 2 if called with -filteropts, 0 else For now, no options are accepted by coqide. there is no way for now to specify a filename that begins with a dash. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13415 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-08-27* scripts/Coqc toplevel/Usage:regisgia
Export the -load-proofs officially. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13388 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-09Fixing part 1 of bug #2242 (-I -as and -R -as were supported forherbelin
coqtop but not coqc). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12911 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-26Coqc: on win32, let's call coqtop.exe by default, not coqtop.opt.exeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12817 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-02Improved parameterization of Coq:herbelin
- add coqtop option "-compat X.Y" so as to provide compatibility with previous versions of Coq (of course, this requires to take care of providing flags for controlling changes of behaviors!), - add support for option names made of an arbitrary length of words (instead of one, two or three words only), - add options for recovering 8.2 behavior for discriminate, tauto, evar unification ("Set Tactic Evars Pattern Unification", "Set Discriminate Introduction", "Set Intuition Iff Unfolding"). Update of .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-26- Suppression date dans configure du trunkherbelin
- Utilisation de get_version_date pour l'option -v (plutôt que la date non à jour du configure) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11714 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin
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
2008-12-12- configure: do not strip coqtop on Darwin so as to support dynamic loadingherbelin
- configure: remove useless newline (hoping it is OK for everyone) - coqc: added option -no-glob in accordance with coqc -usage - coq_makefile: support for installation of all .cmo and all .cmxs in user-contrib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11676 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-22Fixed bug in VernacExtend printing + missing vernacular printing rules +herbelin
revival of option -translate as a -beautify option. PS: compilation checked against 11610. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11618 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-13Tentative d'amélioration de la robustesse des Makefile générés parnotin
coq_makefile en présence de fichiers .ml : - ajout d'une option -config à coqtop qui affiche les informations de configuration (COQTOP, COQBIN, COQLIB, CAMLP4, CAMLP4LIB, CAMLBIN, LOCAL) - coq_makefile inclut un fichier Makefile.config qui contient les valeurs des variables sus-mentionnées git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11584 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-09Suppression d'un warning inutilenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11392 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-07coqc: warning de l'option -dump-glob (unused case)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11315 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-18Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from ↵notin
de coqdoc (compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-24Suppression de l'option -dump-glob et ajout d'une option -no-globnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11167 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-18Uniformisation de l'option -where de coqc avec celle de coqtopnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10235 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-28Remplacement -no-vm par -vmherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7747 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-22compatibility with POWERPCgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-25Added option -no-vm.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6254 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-09-04Correction commit precedentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6062 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03MAJ options coqtop et coqcherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6053 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-18coqc: create_process sous Windowscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5532 85f007b7-540e-0410-9357-904b9bb8a0f7
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
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-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-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-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-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-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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 22:42:45 +0000