From a35f6a25dcc00b3ea15adc4715cff0f98e537005 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 10 Dec 2008 15:16:07 +0000
Subject: 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
---
 contrib/dp/dp_zenon.mll | 4 ++--
 1 file 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
-- 
cgit v1.2.3