diff --git a/.gitignore b/.gitignore
index 80a4d7d4e..554a47d4b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -58,3 +58,4 @@ _minted-*
 *.vtc
 
 *.dot
+*.json
diff --git a/HB/common/database.elpi b/HB/common/database.elpi
index 6ae022a1c..3edc1a5ce 100644
--- a/HB/common/database.elpi
+++ b/HB/common/database.elpi
@@ -1,7 +1,7 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
-shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
+shorten coq.{ term->gref, term-is-gref?, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
 
 %%%%%%%%% HB database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -14,12 +14,29 @@ from_mixin (from _ X _) X.
 pred from_builder i:prop, o:term.
 from_builder (from _ _ X) (global X).
 
+pred has-mixin-instance_cspat i:prop, o:cs-pattern.
+has-mixin-instance_cspat (has-mixin-instance P _ _ _) P.
+
+pred mixin-src_type i:prop, o:term.
+mixin-src_type (mixin-src T _ _ ) T.
+
+pred mixin-src-w-cond_type i:prop, o:term.
+mixin-src-w-cond_type(mixin-src (global G) _ _ :- _) (global G).
+mixin-src-w-cond_type (mixin-src (app [T|_]) _ _ :- _) T.
+mixin-src-w-cond_type (pi x \ (C x)) T :- pi y \ mixin-src-w-cond_type (C y) T.
+
+pred mixin-src_ty i:prop, o:term.
+mixin-src_ty (mixin-src T _ _ ) Ty :-coq.typecheck T Ty ok.
+
 pred mixin-src_mixin i:prop, o:mixinname.
 mixin-src_mixin (mixin-src _ M _) M.
 
 pred mixin-src_src i:prop, o:term.
 mixin-src_src (mixin-src _ _ S) S.
 
+pred mixin-src_srcty i:prop, o:term.
+mixin-src_src (mixin-src _ _ S) Ty :- coq.env.typeof {coq.prod-tgt->gref S} Ty .
+
 pred local-canonical-gref i:prop, o:constant.
 local-canonical-gref (local-canonical C) C.
 
@@ -32,6 +49,9 @@ class_structure (class _ S _) S.
 pred class-def_name i:prop, o:classname.
 class-def_name (class-def (class N _ _)) N.
 
+pred  has-db-instance_type i:prop, o:term.
+ has-db-instance_type (has-db-instance TheType) TheType.
+
 pred mixin-class_class i:prop, o:classname.
 mixin-class_class (mixin-class _ C) C.
 
@@ -133,6 +153,28 @@ factories-provide FLwP MLwP :- std.do! [
   w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP,
 ].
 
+pred undup-grefs  i:list gref, o:list gref.
+undup-grefs  L UL :- std.do! [
+  coq.gref.list->set L S, 
+  coq.gref.set.elements S UL,
+].
+
+pred undup-terms  i:list term, o:list term.
+undup-terms L UL :- std.do! [
+  std.map L coq.term->gref LG,
+  undup-grefs LG ULG,
+  std.map ULG (coq.env.global ) UL,
+].
+
+% % finds all unique types for which an instance was created
+pred findall-cs-types o:list term.
+findall-cs-types TypeList :- std.do![
+  std.findall (has-db-instance _) Clauses,
+  std.map Clauses has-db-instance_type TypeListDup,
+  undup-terms TypeListDup TypeList,
+].
+
+
 % Mixins can be topologically sorted according to their dependencies
 pred toposort-mixins i:list (w-args mixinname), o:list (w-args mixinname).
 toposort-mixins In Out :- std.do! [
@@ -192,10 +234,18 @@ findall-builders LFIL :-
   std.map {std.findall (builder-decl B_)} extract-builder LFILunsorted,
   std.bubblesort LFILunsorted leq-builder LFIL.
 
+pred findall-has-mixin-instance o:list prop.
+findall-has-mixin-instance CL :-
+   std.findall (has-mixin-instance  _ _ _ _) CL.
+
+pred findall-type-src o:list cs-pattern.
+findall-type-src TL :-
+  std.map {std.findall (has-mixin-instance T_ M_ S_ L_)} has-mixin-instance_cspat TL.
+
 pred findall-mixin-src i:term, o:list mixinname.
 findall-mixin-src T ML :-
   std.map {std.findall (mixin-src T M_ V_)} mixin-src_mixin ML.
-
+  
 pred findall-local-canonical o:list constant.
 findall-local-canonical CL :-
   std.map {std.findall (local-canonical C_)} local-canonical-gref CL.
@@ -268,6 +318,7 @@ assert-good-coverage! MLSortedRev CNL :- std.do! [
      true
 ].
 
+
 %%%%% Coq Database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % [get-structure-coercion S1 S2 F] finds the coecion F from the structure S1 to S2
@@ -295,7 +346,7 @@ get-constructor (indt R) (indc K) :- !,
  if (coq.env.indt R _ _ _ _ [K] _) true (coq.error "Not a record" R).
 get-constructor I _ :- coq.error "get-constructor: not an inductive" I.
 
-%% finding for locally defined structures
+% finding for locally defined structures
 pred get-cs-structure i:cs-instance, o:structure.
 get-cs-structure (cs-instance _ _ (const Inst)) Struct :- std.do! [
   coq.env.typeof (const Inst) InstTy,
@@ -309,6 +360,100 @@ get-cs-instance (cs-instance _ _ (const Inst)) Inst.
 pred has-cs-instance i:gref, i:cs-instance.
 has-cs-instance GTy (cs-instance _ (cs-gref GTy) _).
 
+pred param-in-term i:term, i:constant, o:bool.
+param-in-term  (app [global (const F)]) C tt :- (coq.gref->id (const F) ID), (coq.gref->id (const C) ID).
+param-in-term (app [_|Args]) C B :- param-in-term (app Args) C B.
+param-in-term (app []) _ ff.
+param-in-term (prod _ _ F) C B :-  pi x\ param-in-term (F x) C B.
+param-in-term (sort _) _ ff.
+param-in-term T C B :- whd1 T T1, !, param-in-term  T1 C B.
+
+% given a list of section parameters SectionParams and a term T, 
+% returns a list of bool corresponding to whether or not each parameter appears in T.
+pred sect-params-in-term  i:list constant, i:term, o:list bool.
+sect-params-in-term SectionParams T L :-
+  safe-dest-app T (global GR) Args, 
+  factory-alias->gref GR F, factory-nparams F NP, std.split-at NP Args Params _Args2,
+  TyP = app [global GR|Params],
+  std.map SectionParams (x\ o \ param-in-term TyP x o) L.
+
+pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref, o:list bool.
+
+
+pred mixin-src->has-mixin-instance i:list constant, i:prop, o:prop.
+
+mixin-src->has-mixin-instance SectionParams (mixin-src (global GR) M I) (has-mixin-instance (cs-gref GR) M IHd A) :-
+  term->gref I IHd,  coq.typecheck I Ty ok, sect-params-in-term SectionParams Ty A.
+
+mixin-src->has-mixin-instance SectionParams (mixin-src (app [global GR|_] ) M I) (has-mixin-instance (cs-gref GR) M IHd A) :-
+  term->gref I IHd,  coq.typecheck I Ty ok, sect-params-in-term SectionParams Ty A.
+  
+mixin-src->has-mixin-instance SectionParams (mixin-src (prod _ _ _ ) M I) (has-mixin-instance cs-prod M IHd BL):-
+  term->gref I IHd, coq.typecheck I Ty ok, sect-params-in-term SectionParams Ty BL.
+
+mixin-src->has-mixin-instance SectionParams (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd BL):-
+  term->gref I IHd, coq.typecheck I Ty ok, sect-params-in-term SectionParams Ty BL.
+
+
+pred mk-src-aux i:list term, i:term, i:mixinname, i:term, i:list prop, o:prop.
+mk-src-aux [] T M I Cond (mixin-src T M I :- Cond).
+mk-src-aux [A|Rest] T M I Cond ( pi a \ C a) :-
+  pi a \
+  sigma Ta\
+    coq.mk-app T [a] Ta,
+    mk-src-aux Rest Ta M I [coq.unify-eq A a ok|Cond] (C a).
+
+% transforms the has-mixin-instance clause arguments into a
+% mixin-src clause with eventuals conditions regarding its parameters
+pred mk-src
+  i:term, % type of the instance Ty
+  i:mixinname, % name of mixin
+  i:term, % instance body I of type Ty
+  i:list bool, % list of bool for each param, true if they're instance parameters
+  i:list prop, % Cond list
+  o:prop.
+
+mk-src (app [_|Args]) M I [] Cond C :-
+  std.last Args Last,
+  safe-dest-app Last Hd ArgsLast,
+  mk-src-aux ArgsLast Hd M I Cond C.
+
+mk-src (prod N_ _ F) M I [ff|Rest] Cond (pi a \ C a) :-
+  pi a\
+  sigma  Ia \
+  coq.mk-app I [a] Ia,
+    mk-src (F a) M Ia Rest Cond (C a).
+
+mk-src (prod N_ _ F) M I [tt|Rest] Cond C :-
+  sigma a Ia \
+  coq.mk-app I [a] Ia,
+    mk-src (F a) M Ia Rest Cond C.
+
+mk-src (prod N_ _ F) M I [] Cond (pi a \ C a) :-
+  pi a\
+  sigma  Ia \
+  coq.mk-app I [a] Ia,
+    mk-src (F a) M Ia [] Cond (C a).
+
+% for a type T, create as many holes as there are foralls and returns that enriched type
+pred enrich-type i:term, o:term .
+enrich-type T ET :- 
+  coq.typecheck T TH ok,
+  coq.count-prods TH N,
+  if (N = 0) (ET = T) (coq.mk-app T {coq.mk-n-holes N} ET).
+
+% wrapper for mk-src so it can be called by a map on a list of clauses has-mixin-instance
+pred mk-src-map i:prop, o:prop.
+mk-src-map (has-mixin-instance _ M IHd L) C :- std.do![
+  T = global IHd,
+  coq.env.typeof IHd Ty,
+  mk-src Ty M T L [] C,
+  ].
+
+pred cs-pattern->term i:cs-pattern, o:term.
+cs-pattern->term (cs-gref GR) (global GR).
+cs-pattern->term (cs-sort U) (sort U).
+
 pred term->cs-pattern i:term, o:cs-pattern.
 term->cs-pattern (prod _ _ _) cs-prod.
 term->cs-pattern (sort U) (cs-sort U).
diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi
index cd1ffaa4d..85366b424 100644
--- a/HB/common/stdpp.elpi
+++ b/HB/common/stdpp.elpi
@@ -123,6 +123,12 @@ pred coq.env.current-library o:string.
 coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _.
 coq.env.current-library "dummy.v".
 
+pred coq.term-is-gref? i:term, o:gref.
+coq.term-is-gref? (global GR) GR :- !.
+coq.term-is-gref? (pglobal GR _) GR :- !.
+coq.term-is-gref? (app [Hd|_]) GR :- !, coq.term-is-gref? Hd GR.
+coq.term-is-gref? (let _ _ T x\x) GR :- !, coq.term-is-gref? T GR.
+
 pred coq.prod-tgt->gref i:term, o:gref.
 coq.prod-tgt->gref T GR :- whd1 T T1, !, coq.prod-tgt->gref T1 GR.
 coq.prod-tgt->gref (prod N Src Tgt) GR :- !, @pi-decl N Src x\ coq.prod-tgt->gref (Tgt x) GR.
diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi
index 000826a2a..de3993917 100644
--- a/HB/common/utils.elpi
+++ b/HB/common/utils.elpi
@@ -372,4 +372,7 @@ prod-last X X :- !.
 
 pred prod-last-gref i:term, o:gref.
 prod-last-gref (prod N S X) GR :- !, @pi-decl N S x\ prod-last-gref (X x) GR.
-prod-last-gref X GR :- coq.term->gref X GR.
\ No newline at end of file
+prod-last-gref X GR :- coq.term->gref X GR.
+
+pred prod-structure i:term, o:term.
+prod-structure (prod _ S _) S.
\ No newline at end of file
diff --git a/HB/factory.elpi b/HB/factory.elpi
index 2b599df10..ee58687d2 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -53,7 +53,7 @@ argument->w-mixins (ctx-decl Decl) (pr MLwP ArgwP) :- !, std.do! [
 pred argument-name i:argument, o:string.
 argument-name (const-decl Id _ _) Id :- !.
 argument-name (indt-decl (parameter _ _ _ R)) Id :- !,
-  argument-name (indt-decl (R (sort prop))) Id.
+argument-name (indt-decl (R (sort prop))) Id.
 argument-name (indt-decl (record Id _ _ _)) Id :- !.
 argument-name (indt-decl (inductive Id _ _ _)) Id :- !.
 argument-name (ctx-decl _) "_" :- !.
diff --git a/HB/instance.elpi b/HB/instance.elpi
index 0b793248c..156774603 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -14,8 +14,8 @@ declare-existing T0 F0 :- std.do! [
   std.assert! (coq.safe-dest-app FTy (global FactoryAlias) _)
      "The type of the instance is not a factory",
   factory-alias->gref FactoryAlias Factory,
-  private.declare-instance Factory T F Clauses _,
-  acc-clauses current Clauses
+  private.declare-instance Factory T F _ Clauses _,
+  acc-clauses current Clauses,
 ].
 
 % [declare-const N B Ty] adds a Definition N : Ty := B where Ty is a factory
@@ -33,11 +33,12 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
      % A side effect of opening a section is loosing meta data associated
      % with instances, in particular builder tags are lost
      if-verbose (coq.say  "HB: skipping section opening"),
-     SectionBody = Body
+     SectionBody = Body,
+     SectionParams = []
    ) (
     SectionName is "hb_instance_" ^ {std.any->string {new_int}},
     log.coq.env.begin-section SectionName,
-    private.postulate-arity TyWP [] Body SectionBody SectionTy
+    private.postulate-arity TyWP [] Body SectionBody SectionTy SectionParams
   ),
 
   % identify the factory
@@ -66,7 +67,7 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
 
   private.check-non-forgetful-inheritance TheType Factory,
 
-  private.declare-instance Factory TheType TheFactory Clauses CSL,
+  private.declare-instance Factory TheType TheFactory SectionParams Clauses CSL,
 
   % handle parameters via a section -- end
   if (TyWP = arity _) true (
@@ -74,10 +75,77 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
     log.coq.env.end-section-name SectionName
   ),
 
+  % if a clause associated to this type isn't in the database yet we add it
+  
+  if (has-db-instance TheType) true (acc-clause current (has-db-instance TheType)) , 
+  
   % we accumulate clauses now that the section is over
   acc-clauses current Clauses
+
+
+].
+
+% we add a new constructor to terms to represent terms to be abstracted
+type abs int -> term.
+
+% bind back abstracted subterms
+pred bind i:int, i:term, o:term.
+bind M T T1 :- M > 0,
+  T1 = {{ fun x => lp:(B x) }},   
+  N is M - 1,
+  pi x\                           % we allocate the fresh symbol for (abs M)
+    (copy (abs M) x :- !) =>      % we schedule the replacement (abs M) -> x
+    bind N T (B x).
+bind 0 T T1 :- copy T T1.         % we perform all the replacements
+
+% TODO remove see constraints at the end 
+% for a term with M holes, returns a term with M variables to fill these holes
+% the clause see is only generated for a term if it hasn't been seen before
+% 
+pred close-hole-term i:term, o:term.
+close-hole-term T1 T3 :- std.do! [
+  (pi T N M \ fold-map T N (abs M) M :- var T, not (seen T _), !, M is N + 1, see T M) =>
+  (pi T N M \ fold-map T N (abs M) N :- var T, seen T M, !) =>
+  fold-map T1 0 T2 M,
+  bind M T2 T3,
+  % print_constraints,
+  % std.findall (seen _ _) C,
+  % std.forall C (s\ sigma T\ s = see T _, rm-evar T T),
+  % print_constraints,
 ].
 
+
+
+pred seen i:term, o:int.
+% :name "hook1"
+seen X Y :- declare_constraint (seen X Y) [X].  
+
+pred see i:term, o:int.
+see X Y :- declare_constraint (see X Y) [X].
+
+constraint seen see  {
+  % rule (remove X N ) \ (seen uvar X _  _)
+  rule (see (uvar X _) N) \ (seen (uvar X _) M) <=> (M = N). 
+  rule                    \ (seen (uvar X _) _) <=> false. 
+}
+
+pred declare-all2 i:term, i:list class, o:list (pair id constant).
+declare-all2 T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
+
+  enrich-type T Ty,
+  infer_1 Ty Class Struct MLwP S Name _STy Clauses,
+  % infer1 nous donne un term S = (app + Y)
+  % il faut fermer les trous de S
+  % on doit générer un term coq : S' = (fun y => app + y) 
+  close-hole-term S SC,
+  std.assert-ok! (coq.typecheck SC SCTy) "badly closed",
+  save_1 Name SC SCTy CS,
+
+  Clauses => declare-all2 T Rest L.
+
+declare-all2 T [_|Rest] L :- declare-all2 T Rest L.
+declare-all2 _ [] [].
+
 % [declare-all T CL MCSTL] given a type T and a list of class definition
 % CL in topological order (from least dep to most) looks for classes
 % for which all the dependencies (mixins) were postulated so far and skips the
@@ -86,6 +154,19 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
 % Each mixin used in order to fulfill a class is returned together with its name.
 pred declare-all i:term, i:list class, o:list (pair id constant).
 declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
+
+  infer_1 T Class Struct MLwP S Name STy Clauses,
+
+  save_1 Name S STy CS,
+
+  Clauses => declare-all T Rest L.
+
+declare-all T [_|Rest] L :- declare-all T Rest L.
+declare-all _ [] [].
+
+pred infer_1 i:term, i:classname, i:gref, i:factories, o:term, o:string, o:term, o:list prop.
+infer_1 T  Class Struct MLwP S Name STy Clauses:- std.do![
+
   if (not(has-CS-instance? T Struct))
      true % we build it
      (if-verbose (coq.say {header} "skipping already existing"
@@ -101,30 +182,29 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
         {coq.term->string T}))
      fail,
 
-  !,
-
   Name is {cs-pattern->name {term->cs-pattern T}}
     ^ "__canonical__" ^ {gref->modname Struct 2 "_" },
 
   if-verbose (coq.say {header} "declare canonical structure instance" Name),
 
+
   get-constructor Struct KS,
   coq.safe-dest-app T THD _,
   private.optimize-class-body THD {std.length Params} KCApp KCAppNames Clauses,
   coq.mk-app (global KS) {std.append Params [T, KCAppNames]} S,
   if-verbose (coq.say {header} "structure instance for" Name "is" {coq.term->string S}),
-  std.assert-ok! (coq.typecheck S STy) "declare-all: S illtyped",
+  std.assert-ok! (coq.typecheck S STy) "infer1: S illtyped",
+].
+
+pred save_1 i:string, i:term, i:term, i:constant.
+save_1 Name S STy CS:- std.do![
 
   log.coq.env.add-const-noimplicits Name S STy @transparent! CS, % Bug coq/coq#11155, could be a Let
   with-locality (log.coq.CS.declare-instance CS), % Bug coq/coq#11155, should be local
-
   acc-clause current (local-canonical CS),
-
   if-verbose (coq.say {header} "structure instance" Name "declared"),
+].
 
-  Clauses => declare-all T Rest L.
-declare-all T [_|Rest] L :- declare-all T Rest L.
-declare-all _ [] [].
 
 pred declare-factory-sort-deps i:gref.
 declare-factory-sort-deps  GR :- std.do! [
@@ -189,6 +269,21 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [
   declare-const "_" GCF (arity FGCF) CSL
 ].
 
+% create instances for all possible combinations of (simple) types and structure compatible 
+pred saturate-instances.
+saturate-instances :- std.do! [
+  findall-has-mixin-instance ClausesHas,
+  coq.warning "clauseshas : " "debug" ClausesHas,
+  std.map ClausesHas mk-src-map Clauses,
+  std.map-filter Clauses mixin-src-w-cond_type TLD,
+  undup-terms TLD TL,
+  coq.warning "clausessrc : " "debug" Clauses TL,
+  findall-classes Classes,
+  Clauses => std.forall TL (t\ (declare-all2 t Classes _)),
+].
+
+
+
 /* ------------------------------------------------------------------------- */
 /* ----------------------------- private code ------------------------------ */
 /* ------------------------------------------------------------------------- */
@@ -197,9 +292,9 @@ namespace private {
 
 shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
 
-pred declare-instance i:factoryname, i:term, i:term,
+pred declare-instance i:factoryname, i:term, i:term, i:list constant,
   o:list prop, o:list (pair id constant).
-declare-instance Factory T F Clauses CSL :-
+declare-instance Factory T F _SectionParams Clauses CSL :-
   current-mode (builder-from T TheFactory FGR _), !,
   if (get-option "local" tt)
     (coq.error "HB: declare-instance: cannot make builders local.
@@ -207,12 +302,13 @@ declare-instance Factory T F Clauses CSL :-
   !,
   declare-canonical-instances-from-factory-and-local-builders Factory
     T F TheFactory FGR Clauses CSL.
-declare-instance Factory T F Clauses CSL :-
-  declare-canonical-instances-from-factory Factory T F CSL,
+declare-instance Factory T F SectionParams Clauses CSL :-
+  declare-canonical-instances-from-factory Factory T F SectionParams Clauses1 CSL,
   if (get-option "export" tt)
      (coq.env.current-library File,
-      std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses)
-     (Clauses = []).
+      std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2)
+     (Clauses2 = []),
+     std.append Clauses1 Clauses2 Clauses.
 
 % [add-mixin T F _ M Cl] adds a constant being the mixin instance for M on type
 % T built from factory F
@@ -259,18 +355,21 @@ add-all-mixins T FGR ML MakeCanon Clauses CSL :- std.do! [
 % corresponding to parameters in arity A. TS is T applied
 % to all section variables (and hd-beta reduced). Acc should
 % be [] at call site.
-pred postulate-arity i:arity, i:list term, i:term, o:term, o:term.
-postulate-arity (parameter ID _ S A) Acc T T1 Ty :-
+pred postulate-arity i:arity, i:list constant, i:term, o:term, o:term, o:list constant.
+postulate-arity (parameter ID _ S A) Acc T T1 Ty Params :-
   std.assert-ok! (coq.typecheck-ty S _) "arity parameter illtyped",
   if-verbose (coq.say {header} "postulating" ID),
   if (var S) (coq.fresh-type S) true,
   log.coq.env.add-section-variable-noimplicits ID S C,
   Var = global (const C),
-  postulate-arity (A Var) [Var|Acc] T T1 Ty.
-postulate-arity (arity Ty) ArgsRev X T Ty :-
-  hd-beta X {std.rev ArgsRev} X1 Stack1,
+  postulate-arity (A Var) [C|Acc] T T1 Ty Params.
+postulate-arity (arity Ty) ParamsRev X T Ty Params :-
+  std.rev ParamsRev Params,
+  std.map Params (c\o\ o = global (const c)) Args,
+  hd-beta X Args X1 Stack1,
   unwind X1 Stack1 T.
 
+
 % We find the new mixins that F build, we build them and shedule them
 % for becoming builders at section closing time. We also declare
 % all canonical instances these new mixins allow for, so that the user
@@ -284,7 +383,7 @@ declare-canonical-instances-from-factory-and-local-builders
       add-all-mixins T FGR NewMixins ff Clauses MCSL,
   ]),
   list-w-params_list {factory-provides Factory} ML,
-  Clauses => instance.declare-all T {findall-classes-for ML} CCSL,
+  Clauses => declare-all T {findall-classes-for ML} CCSL,
   std.append MCSL CCSL CSL
 ].
 
@@ -292,8 +391,8 @@ declare-canonical-instances-from-factory-and-local-builders
 % it uses all known builders to declare canonical instances of structures
 % on T
 pred declare-canonical-instances-from-factory
-  i:factoryname, i:term, i:term, o:list (pair id constant).
-declare-canonical-instances-from-factory Factory T F CSL :- std.do! [
+  i:factoryname, i:term, i:term, i:list constant, o: list prop, o:list (pair id constant).
+declare-canonical-instances-from-factory Factory T F SectionParams ClausesHas CSL :- std.do! [
   % The order of the following two "under...do!"  is crucial,
   % priority must be given to canonical mixins
   % as they are the ones which guarantee forgetful inheritance
@@ -301,8 +400,12 @@ declare-canonical-instances-from-factory Factory T F CSL :- std.do! [
   synthesis.under-mixin-src-from-factory.do! T F [
     synthesis.under-local-canonical-mixins-of.do! T [
       list-w-params_list {factory-provides Factory} ML,
-      add-all-mixins T Factory ML tt _ MCSL,
-      instance.declare-all T {findall-classes-for ML} CCSL,
+      add-all-mixins T Factory ML tt Clauses MCSL,
+      coq.warning "clausesbef : " "" Clauses,
+      std.map-filter Clauses (mixin-src->has-mixin-instance SectionParams) ClausesHas,
+      coq.warning "clauseshas ; sectionparams : " "" ClausesHas SectionParams,
+      ClausesHas => declare-all T {findall-classes-for ML} CCSL,
+      coq.warning "newclauses " "" CCSL,
     ]
   ],
   std.append MCSL CCSL CSL
diff --git a/HB/structure.elpi b/HB/structure.elpi
index addf308a4..36be56e38 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -210,7 +210,10 @@ declare Module BSkel Sort :- std.do! [
   NewClauses => factory.declare-abbrev Module (factory.by-classname ClassName),
 
   NewClauses => if-MC-compat (private.mc-compat-structure Module ModulePath MLToExport
-    {w-params.nparams MLwP} ClassProjection GRPack)
+    {w-params.nparams MLwP} ClassProjection GRPack),
+
+  NewClauses => instance.saturate-instances,
+
 ].
 
 /* ------------------------------------------------------------------------- */
diff --git a/_CoqProject b/_CoqProject
index b8cf8cf7e..057e90014 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,3 +1,7 @@
 structures.v
 -arg -w -arg -elpi.accumulate-syntax
--Q . HB
\ No newline at end of file
+-arg -w -arg +elpi.typecheck
+-Q . HB
+
+-R tests HB.tests
+-R examples HB.examples
\ No newline at end of file
diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite
index 98c20167e..e2b4e7a55 100644
--- a/_CoqProject.test-suite
+++ b/_CoqProject.test-suite
@@ -3,6 +3,7 @@
 -arg -w -arg -abstract-large-number
 -arg -w -arg -disj-pattern-notation
 -arg -w -arg -notation-overridden
+-arg -w -arg +elpi.typecheck
 
 examples/readme.v
 examples/hulk.v
@@ -72,6 +73,7 @@ tests/not_same_key.v
 tests/hb_pack.v
 tests/declare.v
 tests/short.v
+tests/instance_before_structure.v
 tests/primitive_records.v
 tests/non_forgetful_inheritance.v
 tests/fix_loop.v
@@ -80,6 +82,16 @@ tests/hnf.v
 tests/fun_instance.v
 tests/issue284.v
 tests/issue287.v
+tests/store_types_cs.v
+tests/findall_cs_type.v
+tests/instance_merge_with_distinct_param.v
+tests/instance_merge.v
+
+tests/unit/enrich_type.v
+tests/unit/mixin_src_has_mixin_instance.v
+tests/unit/mk_src_map.v
+tests/unit/close_hole_term.v
+tests/unit/sect_params_in_term.v
 
 -R tests HB.tests
 -R examples HB.examples
diff --git a/instance.md b/instance.md
new file mode 100644
index 000000000..20de63e32
--- /dev/null
+++ b/instance.md
@@ -0,0 +1,53 @@
+<b> Saturating instances on new structure declaration </b>
+
+When a new structure S_new is created, the instances of factories that the new structure implements are not recorded in the database, instead they are in the coq databse. We want to get the list of factories attached to S_new and create properly the instances that implements those factories with the new structure.
+
+See the test file tests/instance_before_structure.v for an example
+
+functions get-canonical-instances and get canonical-structures let us interact with the coq database 
+
+```coq
+1. has-mixin-instance CS-pattern mixinname inst.
+2. mixin-src {{list lp:X}} {{hasmx}} {{i: eq I}} :- coq unification X eqType I (with X = sort I)
+3. has-struct-instance CS-KEY class.
+```
+
+To create the list of booleans we need to have the section paramaters from the instance definition passed down through the clauses, so the information is saved in the database. 
+
+- This list of booleans is created by sect-params-in-term which given a list of section parameters SP and a term T, returns a list of boolean corresponding to whether or not a parameter in SP appears in T.
+
+- This information is crucial in creating the right clauses to saturate the right instances later.
+
+We'll also need later to add parameters from user-created section by interrogating the coq database.
+
+
+Hierarchy builder is supposed to find links within the hierarchy of structures and instances (joins betweens elements).
+
+
+Let's say we have an instance I1 for the structure S1 verifying a mixin M1 and similarly I2, S2, and M2. 
+If we were to introduce a structure S3 which needs a type verifying both M1 and M2 for a type T compatible with I1 and I2, an instance for S3 and T should be generated automatically, and not only upon encountering a new instance. 
+
+So order matters greatly as a new structure wouldn't know about all the previously defined instances, until a new instace is created.
+
+
+Saturating instances works on instances with parameters this way : 
+
+1. For each instance created by the user, we now put a clause in the database called has-mixin-instance, it links some concrete instance I with the mixins it satisfies 
+```coq
+HB.instance Definition I1 : mixin1 nat ... .  
+```
+generates a clause in the database of the form 
+```coq 
+has-mixin-instance (cs-gref (indt «nat»)) (indt «mixin1.axioms_») (const «I1»)
+```
+
+2. Later when we encounter a new structure S, we want to try to populate it with types already encountered at step 1.
+To do so, we look for each possible key-types which satisfy the mixins for S in the has-mixin-instance database. 
+    
+    For those, we create new clauses mixin-src on the fly from the clauses has-mixin-instance which contain the "blueprint" to have the right instance with parameters and the conditions on those parameters.
+    
+    From there if we can create an instance for S we do so by using the coq engine to unify types in the hierarchy.
+
+
+saturate instances could be integrated into the normal program
+test unitaires pour chaque fonction venant de la description complète de cette fonction
\ No newline at end of file
diff --git a/structures.v b/structures.v
index 30c9015f4..8c1fc698e 100644
--- a/structures.v
+++ b/structures.v
@@ -192,6 +192,10 @@ pred mixin-class o:mixinname, o:classname.
 % Coq's CS database (which is just for structures).
 pred mixin-src o:term, o:mixinname, o:term.
 
+
+% states that a certain type has a canonical instance
+pred has-db-instance o:term.
+
 %% database for HB.builders %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % [builder N TheFactory TheMixin S] is used to
@@ -531,6 +535,7 @@ solve (goal _ _ Ty _ Args as G) GLS :- with-attributes (with-logging (std.do! [
 Elpi Typecheck.
 Elpi Export HB.pack.
 
+
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -611,9 +616,10 @@ Elpi Accumulate Db hb.db.
 Elpi Accumulate lp:{{
 
 main [const-decl N (some B) Arity] :- !, std.do! [
+  % compute the universe for the structure (default )
   prod-last {coq.arity->term Arity} Ty,
-  if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort,
-  with-attributes (with-logging (structure.declare N B Univ))
+  if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort, 
+  with-attributes (with-logging (structure.declare N B Univ)),
 ].
 main _ :- coq.error "Usage: HB.structure Definition <ModuleName> := { A of <Factory1> A & … & <FactoryN> A }".
 
@@ -625,6 +631,35 @@ Elpi Export HB.structure.
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 
+(* [HB.saturate_instances] saturates all instances possible *)
+
+
+#[arguments(raw)] Elpi Command HB.saturate_instances.
+#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
+#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
+Elpi Accumulate File "HB/common/stdpp.elpi".
+Elpi Accumulate File "HB/common/database.elpi".
+Elpi Accumulate File "HB/common/utils.elpi".
+Elpi Accumulate File "HB/common/log.elpi".
+Elpi Accumulate File "HB/common/synthesis.elpi".
+Elpi Accumulate File "HB/structure.elpi".
+Elpi Accumulate File "HB/context.elpi".
+Elpi Accumulate File "HB/instance.elpi".
+Elpi Accumulate File "HB/common/phant-abbreviation.elpi".
+Elpi Accumulate File "HB/factory.elpi".
+Elpi Accumulate File "HB/export.elpi".
+Elpi Accumulate Db hb.db.
+Elpi Accumulate lp:{{
+main [] :- !, with-attributes (with-logging (instance.saturate-instances)).
+main _ :- coq.error "Usage: HB.saturate_instances".
+}}.
+Elpi Typecheck.
+Elpi Export HB.saturate_instances.
+
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+
 (** [HB.instance] associates to a type all the structures that can be
     obtained from the provided factory inhabitant.
 
@@ -672,6 +707,7 @@ main _ :- coq.error "Usage: HB.instance Definition <Name> := <Builder> T ...".
 Elpi Typecheck.
 Elpi Export HB.instance.
 
+
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
diff --git a/tests/findall_cs_type.v b/tests/findall_cs_type.v
new file mode 100644
index 000000000..d1c5eed98
--- /dev/null
+++ b/tests/findall_cs_type.v
@@ -0,0 +1,30 @@
+From HB Require Import structures.
+From elpi Require Import elpi.
+
+HB.mixin Record m1 T := { default1 : T }.
+HB.mixin Record m2 T := { default1 : T }.
+HB.mixin Record m3 T := { default2 : T }.
+HB.mixin Record m4 T := { default3 : T }.
+HB.mixin Record m5 T := { default4 : T }.
+(* no types yet*)
+Elpi Query HB.instance lp:{{std.assert! (findall-cs-types []) "a type was found"}}.
+
+
+
+HB.instance Definition _ : m1 nat := m1.Build nat 1.
+HB.instance Definition _ : m2 nat := m2.Build nat 2.
+(*no duplicates *)
+Elpi Query HB.instance lp:{{
+    std.assert! (findall-cs-types [X]) "no type",
+    std.assert! (X = {{nat}}) "wrong type".
+}}.
+
+HB.instance Definition _ : m4 bool := m4.Build bool true.
+HB.instance Definition _ : m5 nat := m5.Build nat 5.
+HB.instance Definition _ : m3 bool := m3.Build bool false.
+Elpi Query HB.instance lp:{{
+    findall-cs-types Clauses,
+    std.assert! (std.length Clauses 2) "wrong number of clauses",
+    std.assert! (X = {{bool}}) "wrong type",
+    std.assert! (Y = {{nat}}) "wrong type".
+}}.
\ No newline at end of file
diff --git a/tests/instance_before_structure.v b/tests/instance_before_structure.v
new file mode 100644
index 000000000..ec8300c90
--- /dev/null
+++ b/tests/instance_before_structure.v
@@ -0,0 +1,37 @@
+From HB Require Import structures.
+
+HB.mixin Record m1 T := { default1 : T }.
+
+HB.mixin Record m2 T := { default2 : T }.
+
+HB.mixin Record m3 T := { default3 : T }.
+
+HB.structure Definition s1  := { T of m1 T }.
+
+HB.instance Definition _ : m1 nat := m1.Build nat 1.
+
+HB.about nat.
+
+(* too early *)
+HB.instance Definition _ : m2 nat := m2.Build nat 2.
+
+HB.about nat. (* only s1 on nat *)
+
+HB.instance Definition _ : m3 nat := m3.Build nat 3.
+
+HB.structure Definition s2 := { T of m1 T & m2 T }.
+HB.about nat. (* s2 is not there yet *)
+
+HB.structure Definition s3 := { T of m3 T }.
+HB.about nat. (* s2 has been instanciated but not s3 *)
+
+
+(* here it works *)
+HB.saturate_instances.
+HB.about nat. (* all there *)
+
+Check @default1 nat.
+Check @default2 nat.
+Check @default3 nat.
+
+
diff --git a/tests/instance_merge.v b/tests/instance_merge.v
new file mode 100644
index 000000000..9e48dff3d
--- /dev/null
+++ b/tests/instance_merge.v
@@ -0,0 +1,20 @@
+From HB Require Import structures.
+
+HB.mixin Record m1 T := { default1 : T }.
+
+HB.mixin Record m2 T := { default2 : T }.
+
+HB.structure Definition s1 := { T of m1 T }.
+HB.structure Definition s2 := { T of m2 T }.
+
+HB.instance Definition _ : m1 nat := m1.Build nat 1.
+HB.instance Definition nat_m2 : m2 nat := m2.Build nat 2.
+
+HB.structure Definition s3 := { T of m1 T & m2 T }.
+
+Check nat:s3.type.
+(* The s3 instance on nat should be synthetized automatically, *)
+(* But since it's defined afterwards, it's not taken into account. *)
+(* A simple recall suffices: *)
+(* HB.instance Definition _ := nat_m2.
+HB.about nat. *)
diff --git a/tests/instance_merge_with_distinct_param.v b/tests/instance_merge_with_distinct_param.v
new file mode 100644
index 000000000..169d5f7bf
--- /dev/null
+++ b/tests/instance_merge_with_distinct_param.v
@@ -0,0 +1,22 @@
+From HB Require Import structures.
+
+HB.mixin Record m1 T := { default1 : T }.
+
+HB.mixin Record m2 T := { default2 : T }.
+
+HB.structure Definition s1 := { T of m1 T }.
+HB.structure Definition s2 := { T of m2 T }.
+
+HB.instance Definition _ (X : s1.type) : m1 (list X) :=
+  m1.Build (list X) (cons default1 nil).
+HB.instance Definition list_m2 (X : s2.type) : m2 (list X) :=
+  m2.Build (list X) (cons default2 nil).
+
+HB.structure Definition s3 := { T of m1 T & m2 T }.
+
+Fail Check list nat:s3.type.
+
+Fail Check fun t : s1.type => (list t : s3.type).
+Fail Check fun t : s2.type => (list t : s3.type).
+Check fun t : s3.type => (list t : s3.type).
+
diff --git a/tests/instance_params_no_type.v b/tests/instance_params_no_type.v
index 5220be111..5fdd953e9 100644
--- a/tests/instance_params_no_type.v
+++ b/tests/instance_params_no_type.v
@@ -1,7 +1,43 @@
 From HB Require Import structures.
 
 HB.mixin Record is_foo P A := { op : P -> A -> A }.
+
+HB.instance Definition nat_foo P := is_foo.Build P nat (fun _ x => x).
+HB.instance Definition list_foo P := is_foo.Build P (list P) (fun _ x => x).
+HB.instance Definition list_foo' P A:= is_foo.Build P (list A) (fun _ x => x).
+
+About list_foo'.
+
 HB.structure Definition foo P := { A of is_foo P A }.
 
-Axiom f : forall T, T -> nat -> nat.
-HB.instance Definition bar P := is_foo.Build P nat (f P).
\ No newline at end of file
+Section try1.
+Variable A : Type.
+(* .... list A ....
+
+(fun A =>   {|
+    foo.sort := list..;
+    foo.class :=
+      {| foo.instance_params_no_type_is_foo_mixin := list_foo A |}
+  |} ).
+
+
+HB.about foo. *)
+
+(* Elpi Trace Browser. *)
+Check nat_foo.
+Check list_foo.
+HB.mixin Record is_b A:= { default : A }.
+Check foo.type.
+Print foo.type.
+Print Module foo.
+Print foo.axioms_.
+(*Elpi Trace Browser. *)
+HB.structure Definition b := { A of is_b A}.
+HB.instance Definition nat_b := is_b.Build nat 0.
+
+HB.mixin Record is_bar (P : b.type) A := { test : P -> A -> A }.
+
+HB.structure Definition bar P := { A of is_bar P A}.
+HB.instance Definition list_bar P := is_bar.Build P (list P)  (fun _ x => x).
+Check list_bar.
+
diff --git a/tests/store_types_cs.v b/tests/store_types_cs.v
new file mode 100644
index 000000000..20ba19e3c
--- /dev/null
+++ b/tests/store_types_cs.v
@@ -0,0 +1,13 @@
+From HB Require Import structures.
+From elpi Require Import elpi.
+HB.mixin Record m1 T := { default1 : T }.
+
+(* no clauses yet*)
+Elpi Query HB.instance lp:{{std.assert! (not (has-db-instance X)) "already has an instance clause"}}.
+
+HB.instance Definition _ : m1 nat := m1.Build nat 1.
+
+Elpi Query HB.instance lp:{{
+    std.assert! (has-db-instance X) "no clause",
+    std.assert! (X = {{nat}}) "wrong type".
+}}.
\ No newline at end of file
diff --git a/tests/unit/close_hole_term.v b/tests/unit/close_hole_term.v
new file mode 100644
index 000000000..6798a79e9
--- /dev/null
+++ b/tests/unit/close_hole_term.v
@@ -0,0 +1,25 @@
+From HB Require Import structures.
+From elpi Require Import elpi.
+From Coq Require Export Setoid.
+
+Elpi Query HB.instance lp:{{
+    X = app [{{list}}, Y],
+    instance.close-hole-term X Z,
+    std.assert! (Z =  {{fun x => list x}} ) "term badly closed"
+}}.
+
+Elpi Query HB.instance lp:{{
+    instance.close-hole-term {{nat}} Z,
+    std.assert! (Z = {{nat}}) "term badly closed"
+}}.
+
+
+Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) : Prop :=
+inj x y : S (f x) (f y) -> R x y.
+
+Elpi Query HB.structure lp:{{
+    Y = {{Inj}}, %Inj has 5 implicit arguments
+    enrich-type Y X,
+    instance.close-hole-term X Z,
+    std.assert! (Z = {{ fun a b c d e => @Inj e d c b a}}) "term badly closed".
+}}.
\ No newline at end of file
diff --git a/tests/unit/enrich_type.v b/tests/unit/enrich_type.v
new file mode 100644
index 000000000..c7ee7bd16
--- /dev/null
+++ b/tests/unit/enrich_type.v
@@ -0,0 +1,27 @@
+From HB Require Import structures.
+From elpi Require Import elpi.
+From Coq Require Export Setoid.
+
+Elpi Query HB.structure lp:{{
+    enrich-type {{nat}} X,
+    std.assert! (X = {{nat}}) "wrong enriched type"
+}}.
+
+Elpi Query HB.structure lp:{{
+    enrich-type {{list}} X,
+    std.assert! (X = app [{{list}}, Y]) "wrong enriched type"
+}}.
+
+Elpi Query HB.structure lp:{{
+    Y = (x \ (y \ {{(prod (list lp:x) (list lp:y))}})),
+    enrich-type (Y _ _) X,
+    std.assert! (X = (app [{{prod}}, (app[{{list}},X1]), app[{{list}},C]])) "wrong enriched type"
+}}.
+
+Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) : Prop :=
+inj x y : S (f x) (f y) -> R x y.
+
+Elpi Query HB.structure lp:{{
+    enrich-type {{Inj}} X,
+    std.assert! (X = app [(global (const Inj)), A, B, R, S, F]) "wrong enriched type"
+}}.
diff --git a/tests/unit/mixin_src_has_mixin_instance.v b/tests/unit/mixin_src_has_mixin_instance.v
new file mode 100644
index 000000000..bee7d2be6
--- /dev/null
+++ b/tests/unit/mixin_src_has_mixin_instance.v
@@ -0,0 +1,31 @@
+From HB Require Import structures.
+From elpi Require Import elpi.
+
+HB.mixin Record m1 T := { default1 : T }.
+HB.mixin Record m2 T := { default2 : T }.
+
+HB.structure Definition s1 := { T of m1 T }.
+HB.instance Definition i1 (X : s1.type) : m1 (list X) :=
+m1.Build (list X) (cons default1 nil).
+
+HB.instance Definition nat_m1 : m1 nat := m1.Build nat 1.
+HB.instance Definition nat_m2 : m2 nat := m2.Build nat 1.
+
+
+Elpi Query HB.instance lp:{{
+mixin-src->has-mixin-instance [] (mixin-src {{nat}} M1 {{nat_m1}}) Y,
+Y = has-mixin-instance (cs-gref {{:gref nat}}) {{:gref m1.phant_axioms}} {{:gref nat_m1}} [].
+
+}}.
+
+Section Test.
+Variable X:s1.type.
+
+Elpi Query HB.instance lp:{{
+coq.env.section L,
+mixin-src->has-mixin-instance L (mixin-src {{list X}} M1 {{i1 X}}) Y,
+Y = has-mixin-instance (cs-gref {{:gref list}}) {{:gref m1.phant_axioms}} {{:gref i1}} [ff].
+
+}}.
+End Test.
+
diff --git a/tests/unit/mk_src_map.v b/tests/unit/mk_src_map.v
new file mode 100644
index 000000000..40d1451d3
--- /dev/null
+++ b/tests/unit/mk_src_map.v
@@ -0,0 +1,28 @@
+From HB Require Import structures.
+
+HB.mixin Record is_foo P A := { op : P -> A -> A }.
+
+HB.instance Definition nat_foo P := is_foo.Build P nat (fun _ x => x).
+
+HB.instance Definition list_foo P := is_foo.Build P (list P) (fun _ x => x).
+
+HB.instance Definition list_foo' P A := is_foo.Build P (list A) (fun _ x => x).
+Check list_foo'.
+Check list_foo.
+
+Elpi Query HB.structure lp:{{
+mk-src-map (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} {{:gref list_foo}} [ff]) MS,
+    MS = (pi a b \ 
+        mixin-src (app [{{list}}, b]) ({{:gref is_foo.axioms_}}) (app [{{list_foo}}, a]) 
+            :- [coq.unify-eq a b ok])
+}}.
+
+Elpi Query HB.structure lp:{{
+mk-src-map (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} {{:gref list_foo'}} [tt, ff]) MS',
+MS' = (pi a b \ 
+    mixin-src (app [{{list}}, b]) {{:gref is_foo.axioms_}} (app [{{list_foo'}}, X, a])
+        :- [coq.unify-eq  a b ok]).
+}}.
+
+HB.structure Definition foo P := { A of is_foo P A }.
+HB.about list.
diff --git a/tests/unit/sect_params_in_term.v b/tests/unit/sect_params_in_term.v
new file mode 100644
index 000000000..08f915203
--- /dev/null
+++ b/tests/unit/sect_params_in_term.v
@@ -0,0 +1,16 @@
+From HB Require Import structures.
+From elpi Require Import elpi.
+
+HB.mixin Record is_foo P A := { op : P -> A -> A }.
+
+
+HB.instance Definition nat_foo P := is_foo.Build P nat (fun _ x => x).
+HB.instance Definition list_foo' P A:= is_foo.Build P (list A) (fun _ x => x).
+HB.instance Definition list_foo P := is_foo.Build P (list P) (fun _ x => x).
+
+Elpi Query HB.instance lp:{{
+has-mixin-instance (cs-gref{{:gref nat}}) M1 {{:gref nat_foo}} [tt],
+has-mixin-instance (cs-gref{{:gref list}}) M {{:gref list_foo}} [tt],
+has-mixin-instance (cs-gref{{:gref list}}) M {{:gref list_foo'}} [tt, ff]
+
+}}.
\ No newline at end of file