diff options
| -rw-r--r-- | pretyping/inductiveops.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ec0ff73062..1ecd4773ae 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -750,8 +750,11 @@ let type_of_projection_knowing_arg env sigma p c ty = syntactic conditions *) let control_only_guard env sigma c = + let c = Evarutil.nf_evar sigma c in let check_fix_cofix e c = - match kind (EConstr.to_constr sigma c) with + (** [c] has already been normalized upfront *) + let c = EConstr.Unsafe.to_constr c in + match kind c with | CoFix (_,(_,_,_) as cofix) -> Inductive.check_cofix e cofix | Fix (_,(_,_,_) as fix) -> |