diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/dp/dp_gappa.ml | 4 | ||||
| -rw-r--r-- | contrib/interface/parse.ml | 2 | ||||
| -rw-r--r-- | contrib/micromega/coq_micromega.ml | 2 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/contrib/dp/dp_gappa.ml b/contrib/dp/dp_gappa.ml index f77f1a5c4..9c035aa85 100644 --- a/contrib/dp/dp_gappa.ml +++ b/contrib/dp/dp_gappa.ml @@ -153,7 +153,7 @@ let call_gappa hl p = let gappa_out2 = temp_file "gappa2" in patch_gappa_proof gappa_out gappa_out2; remove_file gappa_out; - let cmd = sprintf "%s/coqc %s" Coq_config.bindir gappa_out2 in + let cmd = (Filename.concat (Envars.coqbin ()) "coqc") ^ " " ^ gappa_out2 in let out = Sys.command cmd in if out <> 0 then raise GappaProofFailed; let gappa_out3 = temp_file "gappa3" in @@ -164,7 +164,7 @@ let call_gappa hl p = (Filename.chop_suffix gappa_out2 ".v") gappa2; close_out c; let lambda = temp_file "gappa_lambda" in - let cmd = sprintf "%s/coqc %s > %s" Coq_config.bindir gappa_out3 lambda in + let cmd = (Filename.concat (Envars.coqbin ()) "coqc") ^ " " ^ gappa_out3 ^ " > " ^ lambda in let out = Sys.command cmd in if out <> 0 then raise GappaProofFailed; remove_file gappa_out2; remove_file gappa_out3; diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index b551b143c..5de6060f0 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -370,7 +370,7 @@ Libobject.relax true; (let coqdir = try Sys.getenv "COQDIR" with Not_found -> - let coqdir = Coq_config.coqlib in + let coqdir = Envars.coqlib () in if Sys.file_exists coqdir then coqdir else diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml index 890671ab5..e9a8a0e3b 100644 --- a/contrib/micromega/coq_micromega.ml +++ b/contrib/micromega/coq_micromega.ml @@ -1294,7 +1294,7 @@ let call_csdpcert provername poly = output_value ch_to (provername,poly : provername * micromega_polys); close_out ch_to; let cmdname = - List.fold_left Filename.concat Coq_config.coqlib + List.fold_left Filename.concat (Envars.coqlib ()) ["contrib"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in let c = Sys.command (cmdname ^" "^ tmp_to ^" "^ tmp_from) in (try Sys.remove tmp_to with _ -> ()); diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 3c4b01f5b..4ee97813b 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -691,7 +691,7 @@ let _ = end ; Option.iter (fun fn -> - let coqdoc = Coq_config.bindir^"/coqdoc" in + let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in let options = " --html -s --body-only --no-index --latin1 --raw-comments" in let dir = Option.get xml_library_root in let command cmd = |