diff options
| author | filliatr | 2003-06-16 09:08:25 +0000 |
|---|---|---|
| committer | filliatr | 2003-06-16 09:08:25 +0000 |
| commit | 91b3f3cd713817fec36d61bd451011849a590063 (patch) | |
| tree | 174f7b0c5f2547f4b95ac1f0fc51396add78f793 /theories | |
| parent | 49410249a3cbfc62e02b604b0e74fe1aa6db61f5 (diff) | |
Ground depth
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4170 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/FSets/FSetBridge.v | 1 | ||||
| -rw-r--r-- | theories/FSets/FSetRBT.v | 4 |
2 files changed, 5 insertions, 0 deletions
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'. |