From: Claudio Sacerdoti Coen Date: Thu, 30 Jul 2009 10:01:44 +0000 (+0000) Subject: Don't reinvent the wheel. X-Git-Tag: make_still_working~3595 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ddc73f8ac2a7271176d3c0885c3ca1ce7638b816;p=helm.git Don't reinvent the wheel. --- diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 795b85042..ed650a3c3 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -143,7 +143,6 @@ let rec lambda_intros rdb metasenv subst context t args = List.map (fun arg -> arg, NCicTypeChecker.typeof ~metasenv ~subst context arg) args in let context_of_args = context in - let mk_appl = function [] -> assert false | [t] -> t | l -> NCic.Appl l in let rec mk_lambda metasenv subst context n processed_args = function | [] -> let metasenv, _, bo, _ = @@ -155,7 +154,8 @@ let rec lambda_intros rdb metasenv subst context t args = let name = "HBeta"^string_of_int n in let metasenv,_,instance,_ = NCicMetaSubst.mk_meta metasenv context_of_args `Term in - let meta_applied = mk_appl (instance::List.rev processed_args) in + let meta_applied = + NCicUntrusted.mk_appl instance (List.rev processed_args) in let metasenv,subst,_,_ = !refiner_typeof ((rdb :> NRstatus.status)#set_coerc_db NCicCoercion.empty_db) metasenv subst context_of_args meta_applied None in @@ -163,7 +163,8 @@ in unify rdb true metasenv subst context_of_args meta_applied ty in let telescopic_ty = NCicSubstitution.lift n instance in let telescopic_ty = - mk_appl (telescopic_ty :: mk_irl (List.length processed_args)) in + NCicUntrusted.mk_appl + telescopic_ty (mk_irl (List.length processed_args)) in let metasenv, subst, bo = mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1) (arg::processed_args) tail