Merge pull request #288 from math-comp/fix_HB.pack_fun_hirarchy

HB.pack was asserting the key is a type

Author: gares

Changelog.md

@@ -1,5 +1,10 @@
 # Changelog
 
+## UNRELEASED
+
+- **Fix** HB.pack works with structures about functions, and not just
+  types 
+
 ## [1.3.0] - 2022-07-27
 
 Compatible with

HB/pack.elpi

@@ -14,7 +14,10 @@ main Ty Args Instance :- std.do! [
   get-constructor Class KC,
   get-constructor Structure KS,
 
-  std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "HB.pack: not a type",
+  std.assert-ok! (d\
+    (coq.elaborate-ty-skeleton TSkel _ T d, d = ok) ;
+     coq.elaborate-skeleton    TSkel _ T d
+  ) "HB.pack: not a well typed key",
 
   private.elab-factories FactoriesSkel T Factories,
 

_CoqProject.test-suite

@@ -68,7 +68,7 @@ tests/lock.v
 tests/interleave_context.v
 tests/not_same_key.v
 #tests/factory_sort.v
-tests/factory_sort_tac.v
+tests/hb_pack.v
 tests/declare.v
 tests/short.v
 tests/primitive_records.v

tests/factory_sort_tac.v renamed to tests/hb_pack.v

@@ -111,4 +111,15 @@ pose X := Foo.pack T (HasFoo.Build A P T H).
 Check X : Foo.type A P.
 Abort.
 
-End test2.
+End test2.
+
+HB.mixin Record isID T (F : T -> T) := { p : forall x : T, F x = x }.
+HB.structure Definition Fun T := { F of isID T F }.
+
+Goal forall f : nat -> nat, forall p : (forall x, f x = x ), True.
+intros f p.
+pose F := isID.Build nat f p.
+pose T : Fun.type nat := HB.pack f F.
+Check T : Fun.type nat.
+Abort.
+