diff options
Diffstat (limited to 'checker/typeops.ml')
| -rw-r--r-- | checker/typeops.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/checker/typeops.ml b/checker/typeops.ml index 19ede4b9a2..138fe8bc95 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -198,14 +198,13 @@ let judge_of_case env ci pj (c,cj) lfj = (* Projection. *) let judge_of_projection env p c ct = - let pb = lookup_projection p env in + let pty = lookup_projection p env in let (ind,u), args = try find_rectype env ct with Not_found -> error_case_not_inductive env (c, ct) in - assert(eq_ind pb.proj_ind ind); - let ty = subst_instance_constr u pb.proj_type in - substl (c :: List.rev args) ty + let ty = subst_instance_constr u pty in + substl (c :: List.rev args) ty (* Fixpoints. *) |