Don't pass (ignored) implicits to interp_mutual_inductive_constr

2 files changed, 12 insertions, 10 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 5cf2b680ca..b603c54026 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -255,7 +255,7 @@ let inductive_levels env evd arities inds =
   in
   let cstrs_levels, min_levels, sizes =
     CList.split3
-      (List.map2 (fun (_,tys,_) (arity,(ctx,du)) ->
+      (List.map2 (fun (_,tys) (arity,(ctx,du)) ->
         let len = List.length tys in
         let minlev = Sorts.univ_of_sort du in
         let minlev =
@@ -350,28 +350,28 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
   let uvars = Univ.LSet.empty in
   let uvars = Context.Rel.(fold_outside (Declaration.fold_constr merge_universes_of_constr) ctx_params ~init:uvars) in
   let uvars = List.fold_right merge_universes_of_constr arities uvars in
-  let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
+  let uvars = List.fold_right (fun (_,ctypes) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
   Evd.restrict_universe_context sigma uvars
 
 let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
   (* Compute renewed arities *)
   let sigma = Evd.minimize_universes sigma in
   let nf = Evarutil.nf_evars_universes sigma in
-  let constructors = List.map (on_pi2 (List.map nf)) constructors in
+  let constructors = List.map (on_snd (List.map nf)) constructors in
   let arities = List.map EConstr.(to_constr sigma) arities in
   let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in
   let sigma, arities = inductive_levels env_ar_params sigma arities constructors in
   let sigma = Evd.minimize_universes sigma in
   let nf = Evarutil.nf_evars_universes sigma in
   let arities = List.map (on_snd nf) arities in
-  let constructors = List.map (on_pi2 (List.map nf)) constructors in
+  let constructors = List.map (on_snd (List.map nf)) constructors in
   let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
   let arityconcl = List.map (Option.map (fun (_anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in
   let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in
   let uctx = Evd.check_univ_decl ~poly sigma udecl in
 
   (* Build the inductive entries *)
-  let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes,cimpls) ->
+  let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) ->
       let template_candidate () =
         templatearity ||
         let ctor_levels =
@@ -484,9 +484,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
     List.init (List.length indl) EConstr.(fun i -> mkApp (mkRel (i + 1 + nuparams), uargs))
     @ List.init nuparams EConstr.(fun i -> mkRel (i + 1)) in
   let generalize_constructor c = EConstr.Unsafe.to_constr (EConstr.Vars.substnl uparam_subst nparams c) in
+  let cimpls = List.map pi3 constructors in
   let constructors = List.map (fun (cnames,ctypes,cimpls) ->
-                         (cnames,List.map generalize_constructor ctypes,cimpls))
-                       constructors
+      (cnames,List.map generalize_constructor ctypes))
+      constructors
   in
   let ctx_params = ctx_params @ ctx_uparams in
   let userimpls = useruimpls @ userimpls in
@@ -497,9 +498,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   (* Try further to solve evars, and instantiate them *)
   let sigma = solve_remaining_evars all_and_fail_flags env_params sigma in
   let impls =
-    List.map2 (fun indimpls (_,_,cimpls) ->
+    List.map2 (fun indimpls cimpls ->
         indimpls, List.map (fun impls ->
-            userimpls @ impls) cimpls) indimpls constructors
+            userimpls @ impls) cimpls)
+      indimpls cimpls
   in
   let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
   (mie, pl, impls)
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 418d971558..cc104b3762 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -57,7 +57,7 @@ val interp_mutual_inductive_constr
   -> indnames:Names.Id.t list
   -> arities:EConstr.t list
   -> arityconcl:(bool * EConstr.ESorts.t) option list
-  -> constructors:(Names.Id.t list * Constr.constr list * 'a list list) list
+  -> constructors:(Names.Id.t list * Constr.constr list) list
   -> env_ar_params:Environ.env
   (** Environment with the inductives and parameters in the rel_context *)
   -> cumulative:bool