From 673a8375900164e8a843d24c2178d10e86b42dc4 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 7 Oct 2024 17:23:46 +0200 Subject: [PATCH] fix set universe poly --- _CoqProject | 3 ++- examples/list_option.v | 5 ++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/_CoqProject b/_CoqProject index 9fa4f95..36a0474 100644 --- 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 \ No newline at end of file +examples/nat_ind.v +examples/list_option.v \ No newline at end of file diff --git a/examples/list_option.v b/examples/list_option.v index b8a4bc6..b91d63a 100644 --- 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. \ No newline at end of file