diff options
| author | herbelin | 2008-12-10 15:16:07 +0000 |
|---|---|---|
| committer | herbelin | 2008-12-10 15:16:07 +0000 |
| commit | a35f6a25dcc00b3ea15adc4715cff0f98e537005 (patch) | |
| tree | 15713e0c77e12e99a7ef4e053165e6f919865149 | |
| parent | 70af80aad166bc54e4bbc80dfc9427cfee32aae6 (diff) | |
Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of
dp_zenon.ml)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11663 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 2fc2a5f4e1..e15e280db0 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 |