attribute #[unsafe(univ)]

Author: gares

HB/common/utils.elpi

@@ -330,3 +330,12 @@ saturate-type-constructor T ET :-
   coq.typecheck T TH ok,
   coq.count-prods TH N,
   coq.mk-app T {coq.mk-n-holes N} ET.
+
+
+pred with-unsafe-univ i:prop.
+with-unsafe-univ P :- get-option "unsafe.univ" tt, !,
+  coq.option.get ["Universe","Checking"] Old,
+  coq.option.set ["Universe","Checking"] (coq.option.bool ff),
+  P,
+  coq.option.set ["Universe","Checking"] Old.
+with-unsafe-univ P :- P.

HB/structures.v

@@ -660,7 +660,7 @@ main [const-decl N (some B) Arity] :- std.do! [
   % compute the universe for the structure (default )
   prod-last {coq.arity->term Arity} Ty,
   if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort,
-  with-attributes (with-logging (structure.declare N B Univ)),
+  with-attributes (with-logging (with-unsafe-univ (structure.declare N B Univ))),
 ].
 
 }}.