Don't reinvent the wheel.

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 795b8504296249d2e624d8005a776c2cd2eaa4cb..ed650a3c326cd5dedc0ff605f877a638a024453c 100644 (file)
--- 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