diff options
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 930efa5d36..f82b754c59 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -88,13 +88,6 @@ let expmod_constr cache modlist c = let u = Instance.append u' u in let pms = Array.append prefix pms in let ci = { ci with ci_npar = ci.ci_npar + Array.length prefix } in - let iv = match iv with - | NoInvert -> NoInvert - | CaseInvert {univs; args;} -> - let univs = Instance.append u' univs in - let args = Array.append prefix args in - CaseInvert {univs; args;} - in Constr.map substrec (mkCase (ci,u,pms,p,iv,t,br)) | exception Not_found -> Constr.map substrec c |