diff options
| author | Pierre-Marie Pédrot | 2020-08-11 20:01:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-11 20:03:07 +0200 |
| commit | 5aebae7d1762ad44b358f448c9ddc02de3a01f94 (patch) | |
| tree | 1ccc5ec207f977b56b9d24027ab1c53314617091 /pretyping/reductionops.ml | |
| parent | 1d6c794956b962294db765e624b58e531e2f970a (diff) | |
Move reduce_mind_case from Reductionops to Tacred.
It was only used there, and its API required to export an ad-hoc type
to represent pattern-matchings.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index fdc770dba6..06bbd8dcb8 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 @@ -530,18 +523,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})] *) |