From 75508769762372043387c67a9abe94e8f940e80a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 27 Oct 2017 14:03:51 +0200
Subject: Add a non-cumulative impredicative universe SProp.

Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
---
 tools/coq_dune.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tools')

diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index 98368d76ca..fa8b771a74 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -127,6 +127,7 @@ module Options = struct
   let all_opts =
   [ { enabled = false; cmd = "-debug"; }
   ; { enabled = false; cmd = "-native_compiler"; }
+  ; { enabled = true; cmd = "-allow-sprop"; }
   ]
 
   let build_coq_flags () =
-- 
cgit v1.2.3