Open
Description
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.