X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=ed650a3c326cd5dedc0ff605f877a638a024453c;hb=ddc73f8ac2a7271176d3c0885c3ca1ce7638b816;hp=795b8504296249d2e624d8005a776c2cd2eaa4cb;hpb=d1104e488c873c9ae01d3f00d0463ad723f163cd;p=helm.git

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