fix factory-constructor

Author: gares

HB/common/database.elpi

@@ -236,7 +236,7 @@ findall-factory-constructor L :-
   std.map {std.findall (findall-factory-constructor.aux _)} findall-factory-constructor.make L.
 pred findall-factory-constructor.aux o:prop.
 findall-factory-constructor.aux (factory-constructor F C) :-
-  from F _ _, factory-constructor F C.
+  is-factory F, factory-constructor F C.
 func findall-factory-constructor.make prop -> prop.
 findall-factory-constructor.make (findall-factory-constructor.aux P) P.
 

HB/factory.elpi

@@ -299,6 +299,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   log.coq.env.begin-module "Exports" none,
   std.flatten [Clauses, GRDepsClauses, [
+    is-factory (indt R),
     factory-constructor (indt R) GRK,
     factory-nparams (indt R) NParams,
     factory-builder-nparams BuildConst NParams,
@@ -373,7 +374,8 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance
 
   w-params.nparams MLwP NParams,
   std.flatten [ Clauses, GRDepsClauses,
-      [ factory-nparams (const C) NParams,
+      [ is-factory (const C),
+        factory-nparams (const C) NParams,
         factory-constructor (const C) GRK,
         factory-builder-nparams BuildConst NParams,
         % gref-deps GRFSort MLwP,

HB/structures.v

@@ -149,6 +149,9 @@ func factory-nparams factoryname -> int.
 % [is-structure GR] tests if GR is a known structure
 pred is-structure o:gref.
 
+% [is-factory GR] tests if GR is a known factory
+pred is-factory o:gref.
+
 % [factory-builder-nparams Build N] states that when the user writes
 % the [F.Build T] abbreviation the term behind it has N arguments before T
 pred factory-builder-nparams o:constant, o:int.