#[primitive] HB.mixin breaks the types of constants lifting mixin projections #386
Description
Example:
From Coq Require Import ssreflect ssrfun.
From HB Require Import structures.
#[primitive]
HB.mixin Record AddMonoid_of_TYPE S := {
zero : S;
add : S -> S -> S;
addrA : associative add;
add0r : left_id zero add;
addr0 : right_id zero add;
}.
HB.structure Definition AddMonoid := { A of AddMonoid_of_TYPE A }.
Check addrA.
(*
addrA
: associative (AddMonoid_of_TYPE.add _ (AddMonoid.class ?s))
where
?s : [ |- AddMonoid.type]
*)The type of addrA should be associative add.