Skip to content

HB.howto fails with weird error message on mixins, factories and classes. #321

Open
@CohenCyril

Description

@CohenCyril

Example:

From Coq Require Import ZArith ssrfun ssreflect.
From HB Require Import structures.
From HB Require Import demo1.hierarchy_5.

Fail HB.howto AddMonoid_of_TYPE. (* mixin *)
Fail HB.howto Ring_of_TYPE. (* factory *)
Fail HB.howto Ring. (* class *)

fails with error

The command has indeed failed with message:
Not Yet Implemented: complex call to Locate: Ring

it is indeed not yet implemented... but not because of locate.

We should either give it a meaning (signature of the mixin / factory and saying using a class can be used only with .on or .copy ?) or fail with an error message pointing towards the structure of interest (here Ring.type when asking about Ring).

See #322 as a starting point for a fix.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions