aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets/FSetBridge.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FSetBridge.v')
-rw-r--r--theories/FSets/FSetBridge.v1
1 files changed, 1 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]. *)