Merge PR #12823: Move reduce_mind_case from Reductionops to Tacred.

Reviewed-by: gares

3 files changed, 22 insertions, 36 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index fdc770dba6..cb84fd8624 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -499,13 +499,6 @@ let beta_applist sigma (c,l) =
 
 (* Iota reduction tools *)
 
-type 'a miota_args = {
-  mP      : constr;     (* the result type *)
-  mconstr : constr;     (* the constructor *)
-  mci     : case_info;  (* special info to re-build pattern *)
-  mcargs  : 'a list;    (* the constructor's arguments *)
-  mlf     : 'a array }  (* the branch code vector *)
-
 let reducible_mind_case sigma c = match EConstr.kind sigma c with
   | Construct _ | CoFix _ -> true
   | _  -> false
@@ -514,10 +507,7 @@ let contract_cofix sigma (bodynum,(names,types,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
   let make_Fi j =
     let ind = nbodies-j-1 in
-    if Int.equal bodynum ind then mkCoFix (ind,typedbodies)
-    else
-      let bd = mkCoFix (ind,typedbodies) in
-      bd
+    mkCoFix (ind,typedbodies)
   in
   let closure = List.init nbodies make_Fi in
   substl closure bodies.(bodynum)
@@ -530,18 +520,6 @@ let reduce_and_refold_cofix recfun env sigma cofix sk =
     (fun _ (t,sk') -> recfun (t,sk'))
     [] sigma raw_answer sk
 
-let reduce_mind_case sigma mia =
-  match EConstr.kind sigma mia.mconstr with
-    | Construct ((ind_sp,i),u) ->
-(*      let ncargs = (fst mia.mci).(i-1) in*)
-        let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
-        applist (mia.mlf.(i-1),real_cargs)
-    | CoFix cofix ->
-        let cofix_def = contract_cofix sigma cofix in
-        (* XXX Is NoInvert OK here? *)
-        mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
-    | _ -> assert false
-
 (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
    Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
 
@@ -549,10 +527,7 @@ let contract_fix sigma ((recindices,bodynum),(names,types,bodies as typedbodies)
     let nbodies = Array.length recindices in
     let make_Fi j =
       let ind = nbodies-j-1 in
-      if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies)
-      else
-        let bd = mkFix ((recindices,ind),typedbodies) in
-        bd
+      mkFix ((recindices,ind),typedbodies)
     in
     let closure = List.init nbodies make_Fi in
     substl closure bodies.(bodynum)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 0f288cdd46..d404a7e414 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -217,22 +217,14 @@ val splay_prod_n : env ->  evar_map -> int -> constr -> rel_context * constr
 val splay_lam_n : env ->  evar_map -> int -> constr -> rel_context * constr
 (** Raises [Invalid_argument] *)
 
-
-type 'a miota_args = {
-  mP      : constr;     (** the result type *)
-  mconstr : constr;     (** the constructor *)
-  mci     : case_info;  (** special info to re-build pattern *)
-  mcargs  : 'a list;    (** the constructor's arguments *)
-  mlf     : 'a array }  (** the branch code vector *)
-
 val reducible_mind_case : evar_map -> constr -> bool
-val reduce_mind_case : evar_map -> constr miota_args -> constr
 
 val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, EInstance.t) kind_of_term
 val is_arity : env ->  evar_map -> constr -> bool
 val is_sort : env -> evar_map -> types -> bool
 
 val contract_fix : evar_map -> fixpoint -> constr
+val contract_cofix : evar_map -> cofixpoint -> constr
 
 (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
 val is_transparent : Environ.env -> Constant.t tableKey -> bool
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index e4b5dc1edf..9d15e98373 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -458,6 +458,25 @@ let contract_cofix_use_function env sigma f
   substl_checking_arity env (List.rev subbodies)
     sigma (nf_beta env sigma bodies.(bodynum))
 
+type 'a miota_args = {
+  mP      : constr;     (** the result type *)
+  mconstr : constr;     (** the constructor *)
+  mci     : case_info;  (** special info to re-build pattern *)
+  mcargs  : 'a list;    (** the constructor's arguments *)
+  mlf     : 'a array }  (** the branch code vector *)
+
+let reduce_mind_case sigma mia =
+  match EConstr.kind sigma mia.mconstr with
+    | Construct ((ind_sp,i),u) ->
+(*      let ncargs = (fst mia.mci).(i-1) in*)
+        let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
+        applist (mia.mlf.(i-1),real_cargs)
+    | CoFix cofix ->
+        let cofix_def = contract_cofix sigma cofix in
+        (* XXX Is NoInvert OK here? *)
+        mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
+    | _ -> assert false
+
 let reduce_mind_case_use_function func env sigma mia =
   match EConstr.kind sigma mia.mconstr with
     | Construct ((ind_sp,i),u) ->