diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e67aff0021..344ca87fbe 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -165,7 +165,7 @@ let abstract_mind_lc env ntyps npars lc = list_tabulate (function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps in - Array.map (compose (nf_beta env Evd.empty) (substl make_abs)) lc + Array.map (compose nf_beta (substl make_abs)) lc let listrec_mconstr env ntypes hyps nparams i indlc = let nhyps = List.length hyps in |