Skip to content

compilation of monae with hierarchy-builder 1.7.1 #477

@affeldt-aist

Description

@affeldt-aist

We observed that compilation of monae with hierarchy-builder 1.7.1 fails at the following code:

234: #[short(type=nattrans)]
235: HB.structure Definition Nattrans (F G : functor) := {f of isNatural F G f}.
236: Arguments natural {F G} s.
237: Notation "f ~> g" := (nattrans f g) : monae_scope.

with the following error:

File "./theories/core/hierarchy.v", line 234, characters 0-99:
Error:
term->gref: input has no global reference: prod `A` (sort (typ «isNatural.phant_axioms.u0»)) c2 \
 prod `_` (app [global (const «Functor.sort»), c0, c2]) c3 \
  app [global (const «Functor.sort»), c1, c2]

where compilation with 1.7.0 is fine.
@davidnowak

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions