From 48be85eef75634e11545fc24c3afb96fc9abc58d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 Apr 2003 12:07:27 +0000
Subject: Implicit Types

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3978 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Arith/Between.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 20d5e3f7e1..2d5104af26 100755
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -14,6 +14,8 @@ Require Lt.
 V7only [Import nat_scope.].
 Open Local Scope nat_scope.
 
+Implicit Variables Type k,l,p,q,r:nat.
+
 Section Between.
 Variables P,Q : nat -> Prop.
 
-- 
cgit v1.2.3