diff options
| author | herbelin | 2003-08-14 20:43:22 +0000 |
|---|---|---|
| committer | herbelin | 2003-08-14 20:43:22 +0000 |
| commit | 7374c787f4a2bb0d50e2d9348e559b1c94dfff5b (patch) | |
| tree | 6d26b9e249bbb6d8c19a2879cc405a1553ccacb0 | |
| parent | 4135e812a99fdfd7404fd354f31f286a4b4f005a (diff) | |
Fusion -translate et -ftranslate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4276 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile | 7 | ||||
| -rw-r--r-- | scripts/coqc.ml | 4 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 8 |
3 files changed, 8 insertions, 11 deletions
@@ -212,7 +212,8 @@ ML4FILES += contrib/interface/debug_tac.ml4 contrib/interface/centaur.ml4 PARSERREQUIRES=$(CMO) # Solution de facilité... PARSERREQUIRESCMX=$(PARSERREQUIRES:.cmo=.cmx) -ML4FILES += contrib/correctness/psyntax.ml4 contrib/omega/g_omega.ml4 \ +ML4FILES +=\ + contrib/correctness/psyntax.ml4 contrib/omega/g_omega.ml4 \ contrib/romega/g_romega.ml4 contrib/ring/g_quote.ml4 \ contrib/ring/g_ring.ml4 \ contrib/field/field.ml4 contrib/fourier/g_fourier.ml4 \ @@ -717,7 +718,7 @@ CORRECTNESSVO=contrib/correctness/Arrays.vo \ contrib/correctness/Exchange.vo \ contrib/correctness/ArrayPermut.vo \ contrib/correctness/ProgBool.vo contrib/correctness/ProgInt.vo \ - contrib/correctness/Sorted.vo contrib/correctness/Tuples.vo + contrib/correctness/Sorted.vo contrib/correctness/Tuples.vo # contrib/correctness/ProgramsExtraction.vo OMEGAVO = contrib/omega/Omega.vo @@ -1274,7 +1275,7 @@ devel: # 1. Translate the old syntax files and build new syntax theories hierarchy translation:: - @$(MAKE) COQ_XML="-ftranslate -no-strict" world + @$(MAKE) COQ_XML="-translate -no-strict" world @$(MAKE) movenew movenew:: diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 324b291b57..692b86c16c 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -108,8 +108,6 @@ let parse_args () = keep := true ; parse (cfiles,args) rem | ("-verbose" | "--verbose") :: rem -> verbose := true ; parse (cfiles,args) rem - | "-translate" :: rem -> - parse (cfiles,"-ftranslate"::args) rem | "-boot" :: rem -> bindir:= Filename.concat Coq_config.coqtop "bin"; parse (cfiles, "-boot"::args) rem @@ -138,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"|"-xml"|"-v7"|"-v8" as o) :: rem -> + |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-translate" as o) :: rem -> parse (cfiles,o::args) rem | ("-v"|"--version") :: _ -> Usage.version () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 199a520c88..5385644879 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -78,7 +78,9 @@ let add_compile verbose s = Options.make_silent true; compile_list := (verbose,s) :: !compile_list let compile_files () = - List.iter (fun (v,f) -> Vernac.compile v f) (List.rev !compile_list) + List.iter + (fun (v,f) -> with_option translate_file (Vernac.compile v) f) + (List.rev !compile_list) let re_exec_version = ref "" let set_byte () = re_exec_version := "byte" @@ -180,10 +182,6 @@ let parse_args is_ide = | "-no-proofs" :: rem -> Options.dont_load_proofs := true; parse rem | "-translate" :: rem -> make_translate true; parse rem - | "-ftranslate" :: rem -> - make_translate true; - translate_file := true; - parse rem | "-unsafe" :: f :: rem -> add_unsafe f; parse rem | "-unsafe" :: [] -> usage () |