Adapt to rocq-prover/rocq#21438 (PrimRecord record type + has_eta)

Author: TDiazT

template-rocq/src/quoter.ml

@@ -437,7 +437,7 @@ struct
           let projs, acc =
             match mib.Declarations.mind_packets with
             (* TODO handle mutual records *)
-            | [| { mind_record = PrimRecord (id, csts, relevance, ps) } |] ->
+            | [| { mind_record = PrimRecord { id; projections = csts; relevances; tys = ps; has_eta } } |] ->
                 let ctxwolet = Vars.smash_rel_context mib.mind_params_ctxt in
                 let indty = Constr.mkApp (Constr.mkIndU ((t,0),inst),
                                         Context.Rel.instance Constr.mkRel 0 ctxwolet) in
@@ -447,7 +447,7 @@ struct
                   let (ty, acc) = quote_term acc envpars sigma pb in
                   let na = Q.quote_ident (Names.Label.to_id cst) in
                   let rel = Q.quote_relevance rel in
-                  ((na, rel, ty) :: ls, acc)) csts ps relevance ([],acc)
+                  ((na, rel, ty) :: ls, acc)) csts ps relevances ([],acc)
                 in ps, acc
             | _ -> [], acc
           in