diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 849ee225b..f7c739fe6 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -84,10 +84,10 @@ let rec_branch_scheme env isevars (sp,j) recargs cstr = (crec (push_rel (Anonymous,None,t) env) (List.rev (lift_rel_context 1 (List.rev rea)),reca)) | _ -> crec (push_rel d env) (rea,reca) in - mkProd (name, body_of_type c, d) + mkProd (name, c, d) | (name,Some b,c as d)::rea, reca -> - mkLetIn (name,b,body_of_type c,crec (push_rel d env) (rea,reca)) + mkLetIn (name,b, c,crec (push_rel d env) (rea,reca)) | [],[] -> mkExistential isevars env (dummy_loc, InternalHole) | _ -> anomaly "rec_branch_scheme" in |