diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index b40badd7c..f99f34b06 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -298,7 +298,7 @@ let type_of_projection env p c ct = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(eq_mind pb.proj_ind (fst ind)); + assert(MutInd.equal pb.proj_ind (fst ind)); let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in substl (c :: List.rev args) ty |