From 33a2a25a91b390c857d0f4cde786343323558f78 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 19 Jun 2002 13:57:40 +0000
Subject: ProgWf -> Zwf

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

diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 7bcc3a6579..dbae1fce5a 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -109,7 +109,7 @@ let wf_nat_pattern =
   PApp (PRef well_founded, [| PRef nat; PRef lt |])
 (* ["((well_founded Z (Zwf ?1))"] *)
 let wf_z_pattern = 
-  let zwf = ConstRef (coq_constant ["correctness";"ProgWf"] "Zwf") in
+  let zwf = ConstRef (coq_constant ["ZArith";"Zwf"] "Zwf") in
   PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| PMeta (Some 1) |]) |])
 (* ["(and ?1 ?2)"] *)
 let and_pattern = 
-- 
cgit v1.2.3