diff options
Diffstat (limited to 'contrib/dp')
| -rw-r--r-- | contrib/dp/dp_gappa.ml | 6 | ||||
| -rw-r--r-- | contrib/dp/dp_zenon.mll | 4 |
2 files changed, 5 insertions, 5 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; diff --git a/contrib/dp/dp_zenon.mll b/contrib/dp/dp_zenon.mll index 2fc2a5f4..e15e280d 100644 --- a/contrib/dp/dp_zenon.mll +++ b/contrib/dp/dp_zenon.mll @@ -154,7 +154,7 @@ and read_main_proof = parse let s = Coq.fun_def_axiom f vars t in if !debug then Format.eprintf "axiom fun def = %s@." s; let c = constr_of_string gl s in - assert_tac true (Name (id_of_string id)) c gl) + assert_tac (Name (id_of_string id)) c gl) [tclTHEN intros reflexivity; tclIDTAC] let exact_string s gl = @@ -165,7 +165,7 @@ and read_main_proof = parse let interp_lemma l gl = let ty = constr_of_string gl l.l_type in tclTHENS - (assert_tac true (Name (id_of_string l.l_id)) ty) + (assert_tac (Name (id_of_string l.l_id)) ty) [exact_string l.l_proof; tclIDTAC] gl in |