+ (let ty_t =
+ try
+ t (*
+ NCicTypeChecker.typeof ~subst ~metasenv context t*)
+ with
+ NCicTypeChecker.AssertFailure msg ->
+ let exc_to_be =
+ fail_exc metasenv subst context (NCic.Meta (n,lc)) t in
+ pp (lazy "fine typeof (fallimento)");
+ let ft = fix_sorts swap exc_to_be t in
+ if ft == t then
+ (prerr_endline ( ("ILLTYPED: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context t
+ ^ "\nBECAUSE:" ^ Lazy.force msg ^
+ ppcontext ~metasenv ~subst context ^
+ ppmetasenv ~subst metasenv
+ ));
+ assert false)
+ else
+ (try
+ pp (lazy ("typeof: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context ft));
+ NCicTypeChecker.typeof ~subst ~metasenv context ft
+ with NCicTypeChecker.AssertFailure _ ->
+ assert false)
+ | NCicTypeChecker.TypeCheckerFailure _ -> assert false
+ in
+ match NCicReduction.whd ~subst context ty_t with
+ NCic.Sort _ -> metasenv,subst, t
+ | NCic.Meta _ -> metasenv,subst,t (* CSC: TO BE IMPLEMENTED *)
+ | _ -> raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term")))
+ (*CSC: TO BE IMPLEMENTED: UnificationFailure of string Lazy.t;; *)