diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 91b851d12f..6f8b407ae9 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -404,7 +404,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in - let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar ty in + let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in let dcl = (na,Some bd'.uj_val,ty'.utj_val) in type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in let ctxtv = Array.map (type_bl env empty_rel_context) bl in |