From 6a8f392badaf7b736651d8349a4eaced47fa2d5e Mon Sep 17 00:00:00 2001
From: Jasper Hugunin <jasperh@cs.washington.edu>
Date: Fri, 29 Jun 2018 17:31:25 -0700
Subject: Make all parameters implicit

---
 src/Util/GlobalSettings.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/Util/GlobalSettings.v')

diff --git a/src/Util/GlobalSettings.v b/src/Util/GlobalSettings.v
index 001799aa3..f8ab4964f 100644
--- a/src/Util/GlobalSettings.v
+++ b/src/Util/GlobalSettings.v
@@ -5,6 +5,9 @@
     => _ end]. *)
 Global Set Asymmetric Patterns.
 
+(** Enforce uniform parameters *)
+Global Set Uniform Inductive Parameters.
+
 (** Consider also: *)
 (** Judgmental η for records, faster projections *)
 (** Set Primitive Projections. *)
-- 
cgit v1.2.3