Commit 5732b598 authored by Gaspard FEREY's avatar Gaspard FEREY

Cleaning up.

parent 942fa2d2
......@@ -21,9 +21,8 @@ Polymorphic Definition p_pid_pid_expl := @pid (forall A:Type,A->A) (@pid).
Universe i j.
Definition aux : forall A : Type@{i}, A -> A :=
p_pid_pid@{j i}.
About p_pid_pid.
Print Universes.
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment