fix set universe poly

coq-community · Oct 7, 2024 · 673a837 · 673a837
1 parent 2aa9842
commit 673a837
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -37,4 +37,5 @@ examples/summable.v
 examples/trocq_setoid_rewrite.v
 examples/Vector_tuple.v
 examples/misc.v
-examples/nat_ind.v
+examples/nat_ind.v
+examples/list_option.v
diff --git a/examples/list_option.v b/examples/list_option.v
@@ -15,6 +15,8 @@ From Coq Require Import ssreflect.
 From Trocq Require Import Trocq.
 From Trocq Require Import Param_trans Param_list.
 
+Set Universe Polymorphism.
+
 Definition option_to_list {A : Type} (xo : option A) : list A :=
   match xo with
   | None => nil
@@ -105,5 +107,6 @@ Qed.
 Goal forall A B C (xo : option A) (f : A -> B) (g : B -> C),
   omap g (omap f xo) = omap (fun x => g (f x)) xo.
 Proof.
-  trocq. apply map_compose.
+  trocq.
+  apply map_compose.
 Qed.