diff options
| author | Pierre-Marie Pédrot | 2018-07-24 17:58:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-24 17:58:01 +0200 |
| commit | 3599d05a5b3664764f19a794dc69c4e28f2e135d (patch) | |
| tree | ee65c9840649332663491ead6073f1323f4a6fb5 /checker/typeops.ml | |
| parent | 388e65b550a6dd12fa4e59b26e03a831ebd842ce (diff) | |
| parent | 277563ab74a0529c330343479a063f808baa6db4 (diff) | |
Merge PR #7908: Projections use index representation
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. *) |