Fixed a few bugs

[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 460bf2d53161557a2be521002dfbe80c52d0e77a..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
@@ -470,7 +483,6 @@ let smart_apply t unit_eq status g =
   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)
@@ -485,8 +497,8 @@ let smart_apply t unit_eq status g =
       | 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)));
+  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