From 1f95f087d79d6c2c79012921ce68553caf20b090 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 5 Nov 2002 16:59:16 +0000 Subject: Intégration des modifs de la branche mowgli : - 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 --- scripts/coqc.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'scripts') diff --git a/scripts/coqc.ml b/scripts/coqc.ml index cd1898f151..fc1e57d785 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -136,7 +136,7 @@ let parse_args () = | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" - |"-silent"|"-m" as o) :: rem -> + |"-silent"|"-m"|"-xml" as o) :: rem -> parse (cfiles,o::args) rem | ("-v"|"--version") :: _ -> Usage.version () -- cgit v1.2.3