diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /contrib/dp/dp_zenon.mll | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'contrib/dp/dp_zenon.mll')
-rw-r--r-- | contrib/dp/dp_zenon.mll | 4 |
1 files changed, 2 insertions, 2 deletions
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 |