From 05fe6622703b84fde385b0caa19ff9e9886c482d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 18 Mar 2010 07:18:36 +0000 Subject: [PATCH] app of app inside smart application. --- helm/software/components/ng_tactics/nnAuto.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 1d4738d95..460bf2d53 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -468,7 +468,9 @@ let smart_apply t unit_eq status g = (* let ggty = mk_cic_term context gty in *) let status, t = disambiguate status ctx t None in let status,t = term_of_cic_term status t ctx in + let _,_,metasenv,subst,_ = status#obj in let ty = NCicTypeChecker.typeof subst metasenv ctx t in + print(lazy("prima")); let ty,metasenv,args = match gty with | NCic.Const(nref) @@ -478,9 +480,13 @@ let smart_apply t unit_eq status g = NCicMetaSubst.saturate metasenv subst ctx ty 0 in let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in let status = status#set_obj (n,h,metasenv,subst,o) in - let pterm = if args=[] then t else NCic.Appl(t::args) in - debug_print(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm))); - debug_print(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty))); + let pterm = if args=[] then t else + match t with + | NCic.Appl l -> NCic.Appl(l@args) + | _ -> NCic.Appl(t::args) + in + print(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm))); + print(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty))); let eq_coerc = let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in @@ -495,7 +501,7 @@ let smart_apply t unit_eq status g = let _,_,metasenv,subst,_ = status#obj in let _,ctx,jty = List.assoc j metasenv in let jty = NCicUntrusted.apply_subst subst ctx jty in - debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty))); + print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty))); fast_eq_check unit_eq status j with | Error _ as e -> debug_print (lazy "error"); raise e -- 2.39.2