saturate: honor #[export]

Author: gares

HB/instance.elpi

@@ -250,7 +250,7 @@ mk-factory-sort-factory AliasGR CFL CSL :- std.do! [
 ].
 
 % create instances for all possible combinations of types and structure compatible 
-func saturate-instances cs-pattern ->.
+func saturate-instances cs-pattern -> .
 saturate-instances Filter :- std.do! [
 
   findall-has-mixin-instance Filter ClausesHas,
@@ -265,7 +265,11 @@ saturate-instances Filter :- std.do! [
 
   Clauses => std.forall2 TL UKL (t\k\sigma Classes\
     std.filter AllClasses (no-instance-for k) Classes,
-    declare-all-on-type-constructor t Classes _),
+    declare-all-on-type-constructor t Classes CI),
+
+  clauses-for-export CI ClausesExport,
+
+  acc-clauses ClausesExport,
 ].
 
 func no-instance-for cs-pattern, hbclass ->.
@@ -293,11 +297,15 @@ declare-instance Factory T F Clauses CFL CSL :-
     T F TheFactory FGR Clauses CFL CSL.
 declare-instance Factory T F Clauses CFL CSL :-
   declare-canonical-instances-from-factory Factory T F Clauses1 CFL CSL,
-  if (get-option "export" tt)
+  clauses-for-export {std.append CFL CSL} Clauses2,
+  std.append Clauses1 Clauses2 Clauses.
+
+func clauses-for-export list (pair id constant) -> list prop.
+clauses-for-export CL ECL :-
+   if (get-option "export" tt)
      (coq.env.current-library File,
-      std.map {std.append CFL CSL} (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2)
-     (Clauses2 = []),
-     std.append Clauses1 Clauses2 Clauses.
+      std.map CL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) ECL)
+     (ECL = []).
 
 % [add-mixin T F _ M Cl] adds a constant being the mixin instance for M on type
 % T built from factory F