From 5a6c49f8100da35be59cb7381e55d1fb7c8572e6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 6 May 2002 12:02:22 +0000
Subject: Cosmétique

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2668 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/zarith_aux.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/ZArith/zarith_aux.v b/theories/ZArith/zarith_aux.v
index a49c60fb45..04fc70f8a7 100644
--- a/theories/ZArith/zarith_aux.v
+++ b/theories/ZArith/zarith_aux.v
@@ -12,7 +12,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