Downgrading level of infix notations involving \sup.

[helm.git] / helm / software / components / ng_tactics / nnAuto.ml

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 1d4738d952029f98835a93fbefefe7af21516313..7c52a7f72ebf7f0122acc2d8f20f4500d2cc0605 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -161,10 +161,12 @@ let height_of_goals status =
 ;;
 
 (* =============================== paramod =========================== *)
-let solve fast status eq_cache goal =
+let solve f status eq_cache goal =
+(*
   let f = 
     if fast then NCicParamod.fast_eq_check
     else NCicParamod.paramod in
+*)
   let n,h,metasenv,subst,o = status#obj in
   let gname, ctx, gty = List.assoc goal metasenv in
   let gty = NCicUntrusted.apply_subst subst ctx gty in
@@ -205,7 +207,7 @@ let solve fast status eq_cache goal =
 ;;
 
 let fast_eq_check eq_cache status goal =
-  match solve true status eq_cache goal with
+  match solve NCicParamod.fast_eq_check status eq_cache goal with
   | [] -> raise (Error (lazy "no proof found",None))
   | s::_ -> s
 ;;
@@ -254,7 +256,7 @@ let fast_eq_check_tac ~params s =
 ;;
 
 let paramod eq_cache status goal =
-  match solve false status eq_cache goal with
+  match solve NCicParamod.paramod status eq_cache goal with
   | [] -> raise (Error (lazy "no proof found",None))
   | s::_ -> s
 ;;
@@ -264,6 +266,17 @@ let paramod_tac ~params s =
   NTactics.distribute_tac (paramod unit_eq) s
 ;;
 
+let demod eq_cache status goal =
+  match solve NCicParamod.demod status eq_cache goal with
+  | [] -> raise (Error (lazy "no progress",None))
+  | s::_ -> s
+;;
+
+let demod_tac ~params s = 
+  let unit_eq = index_local_equations s#eq_cache s in   
+  NTactics.distribute_tac (demod unit_eq) s
+;;
+
 (*
 let fast_eq_check_tac_all  ~params eq_cache status = 
   let g,_,_ = current_goal status in
@@ -468,6 +481,7 @@ 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
   let ty,metasenv,args = 
     match gty with
@@ -478,9 +492,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
+  noprint(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm)));
+  noprint(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 +513,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