From 91b3f3cd713817fec36d61bd451011849a590063 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 16 Jun 2003 09:08:25 +0000
Subject: Ground depth

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4170 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/FSets/FSetBridge.v | 1 +
 theories/FSets/FSetRBT.v    | 4 ++++
 2 files changed, 5 insertions(+)

diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index d099f8114a..7efc272451 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -13,6 +13,7 @@
 
 Require Export FSetInterface.
 Set Implicit Arguments.
+Set Ground Depth 2.
 
 (** * From non-dependent signature [S] to dependent signature [Sdep]. *)
 
diff --git a/theories/FSets/FSetRBT.v b/theories/FSets/FSetRBT.v
index 791920be79..3ed463f1ef 100644
--- a/theories/FSets/FSetRBT.v
+++ b/theories/FSets/FSetRBT.v
@@ -23,6 +23,8 @@ Open Scope Z_scope.
 Notation "[]" := (nil ?) (at level 1).
 Notation "a :: l" := (cons a l) (at level 1, l at next level).
 
+Set Ground Depth 3.
+
 Module Make [X : OrderedType] <: Sdep with Module E := X.
 
   Module E := X.
@@ -1801,6 +1803,8 @@ Module Make [X : OrderedType] <: Sdep with Module E := X.
 
   (** * Equality test *)
 
+Set Ground Depth 5.
+
   Lemma equal : (s,s':t){ Equal s s' } + { ~(Equal s s') }.
   Proof. 
   Intros s s'.
-- 
cgit v1.2.3