From cb9061d894d516e4607a9237813402d929384b26 Mon Sep 17 00:00:00 2001
From: mohring
Date: Thu, 19 Apr 2001 13:07:42 +0000
Subject: remplace Zarith par ZArith

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

(limited to 'contrib/correctness')

diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 950ef30b53..e53043fb19 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -98,7 +98,7 @@ open Equality
 let nat = IndRef (coq_constant ["Init";"Datatypes"] "nat", 0)
 let lt = ConstRef (coq_constant ["Init";"Peano"] "lt")
 let well_founded = ConstRef (coq_constant ["Init";"Wf"] "well_founded")
-let z = IndRef (coq_constant ["Zarith";"fast_integer"] "Z", 0)
+let z = IndRef (coq_constant ["ZArith";"fast_integer"] "Z", 0)
 let and_ = IndRef (coq_constant ["Init";"Logic"] "and", 0)
 let eq = IndRef (coq_constant ["Init";"Logic"] "eq", 0)
 
-- 
cgit v1.2.3