Adapt to rocq-prover/rocq#19346 (ComInductive flags)

Author: SkySkimmer

src/coq_elpi_HOAS.ml

@@ -3039,23 +3039,28 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
           Univ.Level.Set.union acc
             (universes_of_term state t))
         used (nuparams @ params) in
-    let sigma = restricted_sigma_of used state in
+      let sigma = restricted_sigma_of used state in
+      let flags = {
+        ComInductive.poly;
+        cumulative;
+        template = Some false;
+        auto_prop_lowering = false;
+        finite = finiteness;
+      }
+      in
 
       state, comInductive_interp_mutual_inductive_constr
       env_ar_params sigma arity
         ~sigma
-        ~template:(Some false)
+        ~flags
         ~udecl
         ~variances
         ~ctx_params:(nuparams @ params)
         ~indnames:[itname]
         ~arities:[arity]
         ~constructors:[knames, ktypes]
         ~env_ar_params
-        ~cumulative
-        ~poly
-        ~private_ind
-        ~finite:finiteness |> comInductive_interp_mutual_inductive_constr_post
+        ~private_ind |> comInductive_interp_mutual_inductive_constr_post
       in
     let mind = { mind with
       Entries.mind_entry_record =

src/coq_elpi_arg_HOAS.ml

@@ -233,7 +233,7 @@ let univpoly_of ~poly ~cumulative =
 
   let of_coq_inductive_definition id =
     let open Vernacentries.Preprocessed_Mind_decl in
-    let { flags; typing_flags; private_ind; uniform; inductives } = id in
+    let { flags; udecl; typing_flags; private_ind; uniform; inductives } = id in
     if List.length inductives != 1 then nYI "mutual inductives";
     let inductive = List.hd inductives in
     let (((name),(parameters,non_uniform_parameters),arity,constructors),notations) = inductive in
@@ -243,7 +243,7 @@ let univpoly_of ~poly ~cumulative =
           List.map (function (Vernacexpr.(_,NoCoercion,NoInstance),c) -> c
             | _ -> CErrors.user_err Pp.(str "coercion and instance flags not supported"))
             constructors in
-    let { template; udecl; cumulative; poly; finite } = flags in
+    let { ComInductive.template; cumulative; poly; finite } = flags in
     if template <> None then nYI "raw template polymorphic inductives";
     if udecl <> None then nYI "raw universe polymorphic inductives with universe declaration";
     {
@@ -257,7 +257,7 @@ let univpoly_of ~poly ~cumulative =
     }
   let of_coq_record_definition id =
     let open Vernacentries.Preprocessed_Mind_decl in
-    let { flags; primitive_proj; kind; records; } : record = id in
+    let { flags; udecl; primitive_proj; kind; records; } : record = id in
     if List.length records != 1 then nYI "mutual inductives";
     let open Record.Ast in
     let { name; is_coercion; binders : Constrexpr.local_binder_expr list; cfs; idbuild; sort; default_inhabitant_id : Names.Id.t option; } = List.hd records in
@@ -267,7 +267,7 @@ let univpoly_of ~poly ~cumulative =
       match sort.CAst.v with
       | Constrexpr.CSort s -> s
       | _ -> CErrors.user_err ?loc:sort.CAst.loc Pp.(str "only explicits sorts are supported")) in
-    let { template; udecl; cumulative; poly; finite } = flags in
+    let { ComInductive.template; cumulative; poly; finite } = flags in
     if template <> None then nYI "raw template polymorphic inductives";
     if udecl <> None then nYI "raw universe polymorphic inductives with universe declaration";
     {
@@ -996,6 +996,9 @@ let handle_template_polymorphism = function
   | Some false -> Some false
   | Some true -> err Pp.(str "#[universes(template)] is not supported")
 
+let handle_template_polymorphism flags =
+  { flags with ComInductive.template = handle_template_polymorphism flags.ComInductive.template }
+
 let in_elpi_cmd_synterp ~depth ?calldepth state (x : Cmd.raw) =
   let open Cmd in
   match x with
@@ -1033,11 +1036,11 @@ let in_elpi_cmd ~depth ?calldepth coq_ctx state ~raw (x : Cmd.top) =
       state, t, []
   | RecordDecl (_ist,(glob_sign,raw_rdecl)) ->
       let open Vernacentries.Preprocessed_Mind_decl in
-      let { flags = { template; poly; cumulative; udecl; finite }; primitive_proj; kind; records } = raw_rdecl in
-      let template = handle_template_polymorphism template in
+      let { flags; udecl; primitive_proj; kind; records } = raw_rdecl in
+      let flags = handle_template_polymorphism flags in
       (* Definitional type classes cannot be interpreted using this function (why?) *)
       let kind = if kind = Vernacexpr.Class true then Vernacexpr.Class false else kind in
-      let e = Record.interp_structure ~template udecl kind ~cumulative ~poly ~primitive_proj finite records in
+      let e = Record.interp_structure ~flags udecl kind ~primitive_proj records in
       record_entry2lp ~depth coq_ctx E.no_constraints state ~loose_udecl:(udecl = None) e
   | IndtDecl (_ist,(glob_sign,raw_indt)) when raw ->
       let raw_indt = of_coq_inductive_definition raw_indt in
@@ -1047,14 +1050,14 @@ let in_elpi_cmd ~depth ?calldepth coq_ctx state ~raw (x : Cmd.top) =
       state, t, []
   | IndtDecl (_ist,(glob_sign,raw_indt)) -> 
       let open Vernacentries.Preprocessed_Mind_decl in
-      let { flags = { template; poly; cumulative; udecl; finite }; typing_flags; uniform; private_ind; inductives } = raw_indt in
-      let template = handle_template_polymorphism template in
+      let { flags; udecl; typing_flags; uniform; private_ind; inductives } = raw_indt in
+      let flags = handle_template_polymorphism flags in
       let e =
         match inductives with
         | [mind_w_not] ->
             ComInductive.interp_mutual_inductive ~env:coq_ctx.env
-              ~template ~cumulative ~poly ~uniform ~private_ind ?typing_flags
-              udecl [mind_w_not] finite
+              ~flags ~uniform ~private_ind ?typing_flags
+              udecl [mind_w_not]
         | _ -> nYI "(HOAS) mutual inductives"
       in
       inductive_entry2lp ~depth coq_ctx E.no_constraints state ~loose_udecl:(udecl = None) e