From be6383d39fc8688a40ae5d89f96e2e7808dca513 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 25 Dec 2005 14:10:16 +0000
Subject: Traduction des noms v7 en noms v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7728 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/correctness/psyntax.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 33f84013d7..22c7e204a5 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -145,7 +145,7 @@ let bool_not loc a =
   let d = SApp ( [Variable connective_not ], [a]) in
   w d
 
-let ast_zwf_zero loc = mk_appl loc loc "Zwf" [mk_ref loc "ZERO"]
+let ast_zwf_zero loc = mk_appl loc loc "Zwf" [mk_ref loc "Z0"]
 
 (* program -> Coq AST *)
 
-- 
cgit v1.2.3