aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/Makefile3
-rw-r--r--test-suite/bugs/closed/3125.v27
-rw-r--r--test-suite/bugs/closed/3559.v1
-rw-r--r--test-suite/bugs/closed/3690.v75
-rw-r--r--test-suite/bugs/closed/5347.v10
-rw-r--r--test-suite/bugs/closed/5717.v5
-rw-r--r--test-suite/bugs/closed/HoTT_coq_064.v1
-rwxr-xr-xtest-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh2
-rwxr-xr-xtest-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh2
-rw-r--r--test-suite/output/UnivBinders.out151
-rw-r--r--test-suite/output/UnivBinders.v92
-rw-r--r--test-suite/prerequisite/bind_univs.v5
-rw-r--r--test-suite/success/Notations.v6
-rw-r--r--test-suite/success/Typeclasses.v17
-rw-r--r--test-suite/success/bteauto.v1
-rw-r--r--test-suite/success/polymorphism.v38
16 files changed, 387 insertions, 49 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index f169f86e88..6865dcc768 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -95,7 +95,8 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile
PREREQUISITELOG = prerequisite/admit.v.log \
- prerequisite/make_local.v.log prerequisite/make_notation.v.log
+ prerequisite/make_local.v.log prerequisite/make_notation.v.log \
+ prerequisite/bind_univs.v.log
#######################################################################
# Phony targets
diff --git a/test-suite/bugs/closed/3125.v b/test-suite/bugs/closed/3125.v
new file mode 100644
index 0000000000..797146174d
--- /dev/null
+++ b/test-suite/bugs/closed/3125.v
@@ -0,0 +1,27 @@
+(* Not considering singleton template-polymorphic inductive types as
+ propositions for injection/inversion *)
+
+(* This is also #4560 and #6273 *)
+
+Inductive foo := foo_1.
+
+Goal forall (a b : foo), Some a = Some b -> a = b.
+Proof.
+ intros a b H.
+ inversion H.
+ reflexivity.
+Qed.
+
+(* Check that Prop is not concerned *)
+
+Inductive bar : Prop := bar_1.
+
+Goal
+ forall (a b : bar),
+ Some a = Some b ->
+ a = b.
+Proof.
+ intros a b H.
+ inversion H.
+ Fail reflexivity.
+Abort.
diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v
index da12b68689..5210b27032 100644
--- a/test-suite/bugs/closed/3559.v
+++ b/test-suite/bugs/closed/3559.v
@@ -65,6 +65,7 @@ Axiom path_iff_hprop_uncurried : forall `{IsHProp A, IsHProp B}, (A <-> B) -> A
= B.
Inductive V : Type@{U'} := | set {A : Type@{U}} (f : A -> V) : V.
Axiom is0trunc_V : IsTrunc (trunc_S (trunc_S minus_two)) V.
+Existing Instance is0trunc_V.
Axiom bisimulation : V@{U' U} -> V@{U' U} -> hProp@{U'}.
Axiom bisimulation_refl : forall (v : V), bisimulation v v.
Axiom bisimulation_eq : forall (u v : V), bisimulation u v -> u = v.
diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
index fd9640b890..fa30132ab5 100644
--- a/test-suite/bugs/closed/3690.v
+++ b/test-suite/bugs/closed/3690.v
@@ -3,49 +3,44 @@ Set Printing Universes.
Set Universe Polymorphism.
Definition foo (a := Type) (b := Type) (c := Type) := Type.
Print foo.
-(* foo =
-let a := Type@{Top.1} in
-let b := Type@{Top.2} in let c := Type@{Top.3} in Type@{Top.4}
- : Type@{Top.4+1}
-(* Top.1
- Top.2
- Top.3
- Top.4 |= *) *)
-Check @foo. (* foo@{Top.5 Top.6 Top.7
-Top.8}
- : Type@{Top.8+1}
-(* Top.5
- Top.6
- Top.7
- Top.8 |= *) *)
+(* foo@{Top.2 Top.3 Top.5 Top.6 Top.8 Top.9 Top.10} =
+let a := Type@{Top.2} in let b := Type@{Top.5} in let c := Type@{Top.8} in Type@{Top.10}
+ : Type@{Top.10+1}
+(* Top.2 Top.3 Top.5 Top.6 Top.8 Top.9 Top.10 |= Top.2 < Top.3
+ Top.5 < Top.6
+ Top.8 < Top.9
+ *)
+ *)
+Check @foo. (* foo@{Top.11 Top.12 Top.13 Top.14 Top.15 Top.16
+Top.17}
+ : Type@{Top.17+1}
+(* Top.11 Top.12 Top.13 Top.14 Top.15 Top.16 Top.17 |= Top.11 < Top.12
+ Top.13 < Top.14
+ Top.15 < Top.16
+ *)
+ *)
Definition bar := ltac:(let t := eval compute in foo in exact t).
-Check @bar. (* bar@{Top.13 Top.14 Top.15
-Top.16}
- : Type@{Top.16+1}
-(* Top.13
- Top.14
- Top.15
- Top.16 |= *) *)
-(* The following should fail, since [bar] should only need one universe. *)
-Check @bar@{i j}.
+Check @bar. (* bar@{Top.27}
+ : Type@{Top.27+1}
+(* Top.27 |= *) *)
+
+Check @bar@{i}.
Definition baz (a := Type) (b := Type : a) (c := Type : b) := a -> c.
Definition qux := Eval compute in baz.
-Check @qux. (* qux@{Top.24 Top.25
-Top.26}
- : Type@{max(Top.24+1, Top.26+1)}
-(* Top.24
- Top.25
- Top.26 |= Top.25 < Top.24
- Top.26 < Top.25
- *) *)
-Print qux. (* qux =
-Type@{Top.21} -> Type@{Top.23}
- : Type@{max(Top.21+1, Top.23+1)}
-(* Top.21
- Top.22
- Top.23 |= Top.22 < Top.21
- Top.23 < Top.22
- *) *)
+Check @qux. (* qux@{Top.38 Top.39 Top.40
+Top.41}
+ : Type@{max(Top.38+1, Top.41+1)}
+(* Top.38 Top.39 Top.40 Top.41 |= Top.38 < Top.39
+ Top.40 < Top.38
+ Top.41 < Top.40
+ *) *)
+Print qux. (* qux@{Top.34 Top.35 Top.36 Top.37} =
+Type@{Top.34} -> Type@{Top.37}
+ : Type@{max(Top.34+1, Top.37+1)}
+(* Top.34 Top.35 Top.36 Top.37 |= Top.34 < Top.35
+ Top.36 < Top.34
+ Top.37 < Top.36
+ *) *)
Fail Check @qux@{Set Set}.
Check @qux@{Type Type Type Type}.
(* [qux] should only need two universes *)
diff --git a/test-suite/bugs/closed/5347.v b/test-suite/bugs/closed/5347.v
new file mode 100644
index 0000000000..9267b3eb69
--- /dev/null
+++ b/test-suite/bugs/closed/5347.v
@@ -0,0 +1,10 @@
+Set Universe Polymorphism.
+
+Axiom X : Type.
+(* Used to declare [x0@{u1 u2} : X@{u1}] and [x1@{} : X@{u2}] leaving
+ the type of x1 with undeclared universes. After PR #891 this should
+ error at declaration time. *)
+Axiom x₀ x₁ : X.
+Axiom Xᵢ : X -> Type.
+
+Check Xᵢ x₁. (* conversion test raised anomaly universe undefined *)
diff --git a/test-suite/bugs/closed/5717.v b/test-suite/bugs/closed/5717.v
new file mode 100644
index 0000000000..1bfd917d25
--- /dev/null
+++ b/test-suite/bugs/closed/5717.v
@@ -0,0 +1,5 @@
+Definition foo@{i} (A : Type@{i}) (l : list A) :=
+ match l with
+ | nil => nil
+ | cons _ t => t
+ end.
diff --git a/test-suite/bugs/closed/HoTT_coq_064.v b/test-suite/bugs/closed/HoTT_coq_064.v
index b4c745375f..d02a5f120c 100644
--- a/test-suite/bugs/closed/HoTT_coq_064.v
+++ b/test-suite/bugs/closed/HoTT_coq_064.v
@@ -178,6 +178,7 @@ Definition IsColimit `{Funext} C D (F : Functor D C)
Generalizable All Variables.
Axiom fs : Funext.
+Existing Instance fs.
Section bar.
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
index 378573957e..e48f704a2d 100755
--- a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
@@ -10,7 +10,7 @@ cat > _CoqProject <<EOT
./src/test.mli
EOT
-mkdir src
+mkdir -p src
cat > src/test_plugin.mllib <<EOT
Test
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
index 1b57a356ba..4a8f58655a 100755
--- a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
@@ -11,7 +11,7 @@ cat > _CoqProject <<EOT
./src/test.mli
EOT
-mkdir src
+mkdir -p src
cat > src/test_plugin.mllib <<EOT
Test
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 904ff68aa7..f69379a571 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -1,12 +1,155 @@
+NonCumulative Inductive Empty@{u} : Type@{u} :=
+NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
+
+PWrap has primitive projections with eta conversion.
+For PWrap: Argument scope is [type_scope]
+For pwrap: Argument scopes are [type_scope _]
+punwrap@{u} =
+fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
+ : forall A : Type@{u}, PWrap@{u} A -> A
+(* u |= *)
+
+punwrap is universe polymorphic
+Argument scopes are [type_scope _]
+NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
+
+For RWrap: Argument scope is [type_scope]
+For rwrap: Argument scopes are [type_scope _]
+runwrap@{u} =
+fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap
+ : forall A : Type@{u}, RWrap@{u} A -> A
+(* u |= *)
+
+runwrap is universe polymorphic
+Argument scopes are [type_scope _]
+Wrap@{u} = fun A : Type@{u} => A
+ : Type@{u} -> Type@{u}
+(* u |= *)
+
+Wrap is universe polymorphic
+Argument scope is [type_scope]
+wrap@{u} =
+fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
+ : forall A : Type@{u}, Wrap@{u} A -> A
+(* u |= *)
+
+wrap is universe polymorphic
+Arguments A, Wrap are implicit and maximally inserted
+Argument scopes are [type_scope _]
bar@{u} = nat
: Wrap@{u} Set
(* u |= Set < u
*)
bar is universe polymorphic
-foo@{u Top.8 v} =
-Type@{Top.8} -> Type@{v} -> Type@{u}
- : Type@{max(u+1, Top.8+1, v+1)}
-(* u Top.8 v |= *)
+foo@{u Top.17 v} =
+Type@{Top.17} -> Type@{v} -> Type@{u}
+ : Type@{max(u+1, Top.17+1, v+1)}
+(* u Top.17 v |= *)
foo is universe polymorphic
+Monomorphic mono = Type@{u}
+ : Type@{u+1}
+(* {u} |= *)
+
+mono is not universe polymorphic
+The command has indeed failed with message:
+Universe u already bound.
+foo@{E M N} =
+Type@{M} -> Type@{N} -> Type@{E}
+ : Type@{max(E+1, M+1, N+1)}
+(* E M N |= *)
+
+foo is universe polymorphic
+foo@{Top.16 Top.17 Top.18} =
+Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16}
+ : Type@{max(Top.16+1, Top.17+1, Top.18+1)}
+(* Top.16 Top.17 Top.18 |= *)
+
+foo is universe polymorphic
+NonCumulative Inductive Empty@{E} : Type@{E} :=
+NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
+
+PWrap has primitive projections with eta conversion.
+For PWrap: Argument scope is [type_scope]
+For pwrap: Argument scopes are [type_scope _]
+punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A
+(* K |= *)
+
+punwrap is universe polymorphic
+Argument scopes are [type_scope _]
+punwrap is transparent
+Expands to: Constant Top.punwrap
+The command has indeed failed with message:
+Universe instance should have length 3
+The command has indeed failed with message:
+Universe instance should have length 0
+The command has indeed failed with message:
+This object does not support universe names.
+The command has indeed failed with message:
+Cannot enforce v < u because u < gU < gV < v
+Monomorphic bind_univs.mono = Type@{u}
+ : Type@{u+1}
+(* {u} |= *)
+
+bind_univs.mono is not universe polymorphic
+bind_univs.poly@{u} = Type@{u}
+ : Type@{u+1}
+(* u |= *)
+
+bind_univs.poly is universe polymorphic
+insec@{v} = Type@{u} -> Type@{v}
+ : Type@{max(u+1, v+1)}
+(* v |= *)
+
+insec is universe polymorphic
+insec@{u v} = Type@{u} -> Type@{v}
+ : Type@{max(u+1, v+1)}
+(* u v |= *)
+
+insec is universe polymorphic
+inmod@{u} = Type@{u}
+ : Type@{u+1}
+(* u |= *)
+
+inmod is universe polymorphic
+SomeMod.inmod@{u} = Type@{u}
+ : Type@{u+1}
+(* u |= *)
+
+SomeMod.inmod is universe polymorphic
+inmod@{u} = Type@{u}
+ : Type@{u+1}
+(* u |= *)
+
+inmod is universe polymorphic
+Applied.infunct@{u v} =
+inmod@{u} -> Type@{v}
+ : Type@{max(u+1, v+1)}
+(* u v |= *)
+
+Applied.infunct is universe polymorphic
+axfoo@{i Top.33 Top.34} : Type@{Top.33} -> Type@{i}
+(* i Top.33 Top.34 |= *)
+
+axfoo is universe polymorphic
+Argument scope is [type_scope]
+Expands to: Constant Top.axfoo
+axbar@{i Top.33 Top.34} : Type@{Top.34} -> Type@{i}
+(* i Top.33 Top.34 |= *)
+
+axbar is universe polymorphic
+Argument scope is [type_scope]
+Expands to: Constant Top.axbar
+axfoo' : Type@{Top.36} -> Type@{i}
+
+axfoo' is not universe polymorphic
+Argument scope is [type_scope]
+Expands to: Constant Top.axfoo'
+axbar' : Type@{Top.36} -> Type@{i}
+
+axbar' is not universe polymorphic
+Argument scope is [type_scope]
+Expands to: Constant Top.axbar'
+The command has indeed failed with message:
+When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block).
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 8656ff1a39..116d5e5e94 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -2,12 +2,100 @@ Set Universe Polymorphism.
Set Printing Universes.
Unset Strict Universe Declaration.
-Class Wrap A := wrap : A.
+(* universe binders on inductive types and record projections *)
+Inductive Empty@{u} : Type@{u} := .
+Print Empty.
-Instance bar@{u} : Wrap@{u} Set. Proof nat.
+Set Primitive Projections.
+Record PWrap@{u} (A:Type@{u}) := pwrap { punwrap : A }.
+Print PWrap.
+Print punwrap.
+
+Unset Primitive Projections.
+Record RWrap@{u} (A:Type@{u}) := rwrap { runwrap : A }.
+Print RWrap.
+Print runwrap.
+
+(* universe binders also go on the constants for operational typeclasses. *)
+Class Wrap@{u} (A:Type@{u}) := wrap : A.
+Print Wrap.
+Print wrap.
+
+(* Instance in lemma mode used to ignore the binders. *)
+Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed.
Print bar.
(* The universes in the binder come first, then the extra universes in
order of appearance. *)
Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
Print foo.
+
+(* Binders even work with monomorphic definitions! *)
+Monomorphic Definition mono@{u} := Type@{u}.
+Print mono.
+
+(* fun x x => foo is nonsense with local binders *)
+Fail Definition fo@{u u} := Type@{u}.
+
+(* Using local binders for printing. *)
+Print foo@{E M N}.
+(* Underscores discard the name if there's one. *)
+Print foo@{_ _ _}.
+
+(* Also works for inductives and records. *)
+Print Empty@{E}.
+Print PWrap@{E}.
+
+(* Also works for About. *)
+About punwrap@{K}.
+
+(* Instance length check. *)
+Fail Print foo@{E}.
+Fail Print mono@{E}.
+
+(* Not everything can be printed with custom universe names. *)
+Fail Print Coq.Init.Logic@{E}.
+
+(* Nice error when constraints are impossible. *)
+Monomorphic Universes gU gV. Monomorphic Constraint gU < gV.
+Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat.
+
+(* Universe binders survive through compilation, sections and modules. *)
+Require bind_univs.
+Print bind_univs.mono.
+Print bind_univs.poly.
+
+Section SomeSec.
+ Universe u.
+ Definition insec@{v} := Type@{u} -> Type@{v}.
+ Print insec.
+End SomeSec.
+Print insec.
+
+Module SomeMod.
+ Definition inmod@{u} := Type@{u}.
+ Print inmod.
+End SomeMod.
+Print SomeMod.inmod.
+Import SomeMod.
+Print inmod.
+
+Module Type SomeTyp. Definition inmod := Type. End SomeTyp.
+Module SomeFunct (In : SomeTyp).
+ Definition infunct@{u v} := In.inmod@{u} -> Type@{v}.
+End SomeFunct.
+Module Applied := SomeFunct(SomeMod).
+Print Applied.infunct.
+
+(* Multi-axiom declaration
+
+ In polymorphic mode the domain Type gets separate universes for the
+ different axioms, but all axioms have to declare all universes. In
+ polymorphic mode they get the same universes, ie the type is only
+ interpd once. *)
+Axiom axfoo@{i+} axbar : Type -> Type@{i}.
+Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}.
+
+About axfoo. About axbar. About axfoo'. About axbar'.
+
+Fail Axiom failfoo failbar@{i} : Type.
diff --git a/test-suite/prerequisite/bind_univs.v b/test-suite/prerequisite/bind_univs.v
new file mode 100644
index 0000000000..f17c00e9d7
--- /dev/null
+++ b/test-suite/prerequisite/bind_univs.v
@@ -0,0 +1,5 @@
+(* Used in output/UnivBinders.v *)
+
+Monomorphic Definition mono@{u} := Type@{u}.
+
+Polymorphic Definition poly@{u} := Type@{u}.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index e3f90f6d94..3c0ad20700 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -147,3 +147,9 @@ Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x
Fail Check {x@{u},y|x=x}.
Fail Check {?[n],y|0=0}.
+
+(* Check that 10 is well declared left associative *)
+
+Section C.
+Notation "f $$$ x" := (id f x) (at level 10, left associativity).
+End C.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 6b1f0315bc..cd6eac35cf 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -240,3 +240,20 @@ Module IterativeDeepening.
Qed.
End IterativeDeepening.
+
+Module AxiomsAreInstances.
+ Set Typeclasses Axioms Are Instances.
+ Class TestClass1 := {}.
+ Axiom testax1 : TestClass1.
+ Definition testdef1 : TestClass1 := _.
+
+ Unset Typeclasses Axioms Are Instances.
+ Class TestClass2 := {}.
+ Axiom testax2 : TestClass2.
+ Fail Definition testdef2 : TestClass2 := _.
+
+ (* we didn't break typeclasses *)
+ Existing Instance testax2.
+ Definition testdef2 : TestClass2 := _.
+
+End AxiomsAreInstances.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 3178c6fc15..730b367d60 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -55,6 +55,7 @@ Module Backtracking.
Axiom A : Type.
Existing Class A.
Axioms a b c d e: A.
+ Existing Instances a b c d e.
Ltac get_value H := eval cbv delta [H] in H.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 7eaafc3545..d76b307914 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -190,6 +190,8 @@ Module binders.
Fail Defined.
Abort.
+ Fail Lemma bar@{u v | } : let x := (fun x => x) : Type@{u} -> Type@{v} in nat.
+
Lemma bar@{i j| i < j} : Type@{j}.
Proof.
exact Type@{i}.
@@ -200,6 +202,10 @@ Module binders.
exact Type@{i}.
Qed.
+ Monomorphic Universe M.
+ Fail Definition with_mono@{u|} : Type@{M} := Type@{u}.
+ Definition with_mono@{u|u < M} : Type@{M} := Type@{u}.
+
End binders.
Section cats.
@@ -399,6 +405,31 @@ Module Anonymous.
End Anonymous.
+Module Restrict.
+ (* Universes which don't appear in the term should be pruned, unless they have names *)
+ Set Universe Polymorphism.
+
+ Ltac exact0 := let x := constr:(Type) in exact 0.
+ Definition dummy_pruned@{} : nat := ltac:(exact0).
+
+ Definition named_not_pruned@{u} : nat := 0.
+ Check named_not_pruned@{_}.
+
+ Definition named_not_pruned_nonstrict : nat := ltac:(let x := constr:(Type@{u}) in exact 0).
+ Check named_not_pruned_nonstrict@{_}.
+
+ Lemma lemma_restrict_poly@{} : nat.
+ Proof. exact0. Defined.
+
+ Unset Universe Polymorphism.
+ Lemma lemma_restrict_mono_qed@{} : nat.
+ Proof. exact0. Qed.
+
+ Lemma lemma_restrict_abstract@{} : nat.
+ Proof. abstract exact0. Qed.
+
+End Restrict.
+
Module F.
Context {A B : Type}.
Definition foo : Type := B.
@@ -430,3 +461,10 @@ Section test_letin_subtyping.
Qed.
End test_letin_subtyping.
+
+Module ObligationRegression.
+ (** Test for a regression encountered when fixing obligations for
+ stronger restriction of universe context. *)
+ Require Import CMorphisms.
+ Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _ _ _ _}.
+End ObligationRegression.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 02:48:00 +0000