diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ce445c3f6d..9e962267db 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -901,7 +901,7 @@ let internalise sigma globalenv env allow_patvar lvar c = (* Now compact "(f args') args" *) | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args) | _ -> RApp (loc, c, args)) - | CCases (loc, rtnpo, tms, eqns) -> + | CCases (loc, sty, rtnpo, tms, eqns) -> let tms,env' = List.fold_right (fun citm (inds,env) -> let (tm,ind),nal = intern_case_item env citm in @@ -909,7 +909,7 @@ let internalise sigma globalenv env allow_patvar lvar c = tms ([],env) in let rtnpo = Option.map (intern_type env') rtnpo in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in - RCases (loc, rtnpo, tms, List.flatten eqns') + RCases (loc, sty, rtnpo, tms, List.flatten eqns') | CLetTuple (loc, nal, (na,po), b, c) -> let env' = reset_tmp_scope env in let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in @@ -917,11 +917,6 @@ let internalise sigma globalenv env allow_patvar lvar c = let p' = Option.map (intern_type env'') po in RLetTuple (loc, nal, (na', p'), b', intern (List.fold_left (push_name_env lvar) env nal) c) - | CLetPattern (loc, p, c, b) -> - let loc' = cases_pattern_expr_loc p in - let (tm,ind), nal = intern_case_item env (c,(None,None)) in - let eqn' = intern_eqn 1 env (loc, [loc',[p]], b) in - RLetPattern (loc, (tm,ind), List.hd eqn') | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in |