From dfe152b89af9239899e32b2a31adbfda44af5efe Mon Sep 17 00:00:00 2001
From: delahaye
Date: Tue, 9 Jan 2001 16:29:56 +0000
Subject: Meta Definition ->  Tactic Definition

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1239 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Lists/Streams.v     | 2 +-
 theories/Zarith/zarith_aux.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 297a888ebe..5962e0ed2f 100755
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -61,7 +61,7 @@ CoInductive EqSt  : Stream->Stream->Prop :=
 
 (* A coinduction principle *)
 
-Meta Definition CoInduction proof := 
+Tactic Definition CoInduction proof := 
   Cofix proof; Intros; Constructor;
     [Clear proof | Try (Apply proof;Clear proof)].
 
diff --git a/theories/Zarith/zarith_aux.v b/theories/Zarith/zarith_aux.v
index b67bf39f5e..113a593471 100644
--- a/theories/Zarith/zarith_aux.v
+++ b/theories/Zarith/zarith_aux.v
@@ -11,7 +11,7 @@
 Require Arith.
 Require Export fast_integer.
 
-Meta Definition ElimCompare com1 com2:=
+Tactic Definition ElimCompare com1 com2:=
   Elim (Dcompare (Zcompare com1 com2)); [
          Idtac 
        | Intro hidden_auxiliary; Elim hidden_auxiliary; 
-- 
cgit v1.2.3