File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 11structures.v
22theories/cat.v
3- theories/algebra .v
3+ theories/encatD .v
44-arg -w -arg -elpi.accumulate-syntax
55-arg -w -arg +elpi.typecheck
66-Q . HB
Original file line number Diff line number Diff line change @@ -498,7 +498,7 @@ HB.structure Definition UFunctor : Set := {C of UPreFunctor_IsFunctor C}.
498498Set Universe Checking.
499499
500500Unset Universe Checking.
501- HB.about Functor.
501+ (* HB.about Functor. *)
502502HB.structure Definition STUFunctor : Set :=
503503 {C of SFunctor C & TFunctor C & UFunctor C}.
504504Set Universe Checking.
Original file line number Diff line number Diff line change 11Require Import ssreflect ssrfun.
22Unset Universe Checking.
3- From HB Require Import structures cat.
3+ From HB Require Import structures cat encatD .
44Set Universe Checking.
55Require Import Coq.Program .Equality .
66
You can’t perform that action at this time.
0 commit comments