diff options
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'. |