diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index f60e2dbe0f..ac4efc515d 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -653,7 +653,7 @@ let check_one_fix renv recpos def = (* if [t] does not make recursive calls, it is guarded: *) if noccur_with_meta renv.rel_min nfi t then () else - let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in + let (f,l) = decompose_app (whd_betaiotazeta t) in match kind_of_term f with | Rel p -> (* Test if [p] is a fixpoint (recursive call) *) |