summaryrefslogtreecommitdiff
path: root/contrib/dp/dp_gappa.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/dp/dp_gappa.ml')
-rw-r--r--contrib/dp/dp_gappa.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/dp/dp_gappa.ml b/contrib/dp/dp_gappa.ml
index 70439a97..9c035aa8 100644
--- a/contrib/dp/dp_gappa.ml
+++ b/contrib/dp/dp_gappa.ml
@@ -153,18 +153,18 @@ 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
let c = open_out gappa_out3 in
let gappa2 = Filename.chop_suffix (Filename.basename gappa_out2) ".v" in
Printf.fprintf c
- "Require \"%s\". Set Printing Depth 9999999. Print %s.proof."
+ "Require \"%s\". Set Printing Depth 999999. Print %s.proof."
(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;