Adapt to coq/coq#17795 (ComInductive API and glob_sort changes)

LPCIC · Sep 5, 2023 · 4a1c8ae · 4a1c8ae
1 parent 2aeae2e
commit 4a1c8ae
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
@@ -2799,7 +2799,7 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
       let arityconcl =
         match Reductionops.sort_of_arity env_ar_params sigma arity with
         | exception Reduction.NotArity -> None
-        | s -> Some (false,s) in
+        | s -> Some s in
 
     (* restruction to used universes *)
     let state = minimize_universes state in
@@ -2831,7 +2831,7 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
         ~indnames:[itname]
         ~arities:[arity]
         ~arityconcl:[arityconcl]
-        ~constructors:[knames, List.map (EC.to_constr sigma) ktypes]
+        ~constructors:[knames, ktypes]
         ~env_ar_params
         ~cumulative
         ~poly

diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml
@@ -250,7 +250,7 @@ let raw_record_decl_to_glob glob_sign ({ name; sort; parameters; constructor; fi
   let name, space = sep_last_qualid name in
   let sort = match sort with
     | Some x -> Constrexpr.CSort x
-    | None -> Constrexpr.(CSort (Glob_term.UAnonymous {rigid=true})) in
+    | None -> Constrexpr.(CSort (Glob_term.UAnonymous {rigid=UnivRigid})) in
   let intern_env, params = intern_global_context glob_sign ~intern_env:Constrintern.empty_internalization_env parameters in
   let glob_sign_params = push_glob_ctx params glob_sign in
   let params = List.rev params in
@@ -277,7 +277,7 @@ let raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform
   let name = Names.Id.of_string name in
   let indexes = match arity with
     | Some x -> x
-    | None -> CAst.make Constrexpr.(CSort (Glob_term.UAnonymous {rigid=true})) in
+    | None -> CAst.make Constrexpr.(CSort (Glob_term.UAnonymous {rigid=UnivRigid})) in
   let intern_env, params = intern_global_context glob_sign ~intern_env:Constrintern.empty_internalization_env parameters in
   let nuparams_given, nuparams =
     match non_uniform_parameters with

diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml
@@ -164,7 +164,7 @@ let rec gterm2lp ~depth state x =
           Pp.(str"Free Coq variable " ++ Names.Id.print id ++ str " in context: " ++
             prlist_with_sep spc Id.print (Id.Map.bindings ctx.name2db |> List.map fst));
       state, E.mkConst (Id.Map.find id ctx.name2db)
-  | GSort(UAnonymous {rigid=true}) ->
+  | GSort(UAnonymous {rigid=UnivRigid}) ->
       let state, f = F.Elpi.make state in
       let s = API.RawData.mkUnifVar f ~args:[] state in
       state, in_elpi_flex_sort s