From 13e847b7092d53ffec63e4cba54c67d39560e67a Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 15 Feb 2016 23:33:01 +0100 Subject: CLEANUP: Simplifying the changes done in "checker/*" --- checker/inductive.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'checker/inductive.ml') 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 -- cgit v1.2.3