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/inductive.ml | |
| parent | 97d6583a0b9a65080639fb02deba4200f6276ce6 (diff) | |
CLEANUP: Simplifying the changes done in "checker/*"
Diffstat (limited to 'checker/inductive.ml')
| -rw-r--r-- | checker/inductive.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index 948012421..5e2e14f7f 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -634,8 +634,9 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let mib = Environ.lookup_mind mind env in let ntypes = mib.mind_ntypes in let push_ind specif env = - push_rel (LocalAssum (Anonymous, - hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar)) env + let decl = LocalAssum (Anonymous, + hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in + push_rel decl env in let env = Array.fold_right push_ind mib.mind_packets env in let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in |