From ddc73f8ac2a7271176d3c0885c3ca1ce7638b816 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Jul 2009 10:01:44 +0000 Subject: [PATCH 1/1] Don't reinvent the wheel. --- helm/software/components/ng_refiner/nCicUnification.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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 -- 2.39.2