diff options
Diffstat (limited to 'pretyping/detyping.ml')
-rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 3d5a5f025..d4e156fa4 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -504,7 +504,7 @@ let rec detype flags avoid env sigma t = let pb = Environ.lookup_projection p (snd env) in let body = pb.Declarations.proj_body in let ty = Retyping.get_type_of (snd env) sigma (EConstr.of_constr c) in - let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma (EConstr.of_constr ty) in + let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in let args = List.map EConstr.Unsafe.to_constr args in let body' = strip_lam_assum body in let body' = subst_instance_constr u body' in |