diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-15 23:33:01 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-15 23:33:01 +0100 |
| commit | 13e847b7092d53ffec63e4cba54c67d39560e67a (patch) | |
| tree | 9303e5293a739b6bf77b6557da523ab4c3b171d7 /checker/indtypes.ml | |
| parent | 97d6583a0b9a65080639fb02deba4200f6276ce6 (diff) | |
CLEANUP: Simplifying the changes done in "checker/*"
Diffstat (limited to 'checker/indtypes.ml')
| -rw-r--r-- | checker/indtypes.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index f11fa5a7a..566df673c 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -319,7 +319,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = let nhyps = List.length hyps in let rec check k index = function | [] -> () - | LocalDef (_,_,_) :: hyps -> check k (index+1) hyps + | LocalDef _ :: hyps -> check k (index+1) hyps | _::hyps -> match whd_betadeltaiota env lpar.(k) with | Rel w when w = index -> check (k-1) (index+1) hyps @@ -376,8 +376,9 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) = let auxntyp = 1 in let specif = lookup_mind_specif env mi in let env' = - push_rel (LocalAssum (Anonymous, - hnf_prod_applist env (type_of_inductive env (specif,u)) lpar)) env in + let decl = LocalAssum (Anonymous, + hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) in + push_rel decl env in let ra_env' = (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in |