Removed some dead code.

diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml
index 201f522d05420ba5ad8e01152ce65abb940d24e8..a85c18205d7a6aef840fc44eca134b8867d7476c 100644 (file)
--- a/matitaB/components/ng_tactics/nnAuto.ml
+++ b/matitaB/components/ng_tactics/nnAuto.ml
@@ -1174,130 +1174,9 @@ let applicative_case depth signature status flags gty cache =
     try_candidates false 2 elems smart_candidates_other
 ;;
 
-
-(*
-let get_candidates ?(smart=true) depth flags status cache signature gty =
-  let maxd = ((depth + 1) = flags.maxdepth) in 
-  let universe = status#auto_cache in
-  let _,_,metasenv,subst,_ = status#obj in
-  let context = ctx_of gty in
-  let _, raw_gty = term_of_cic_term status gty context in
-  debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
-  let raw_weak_gty, weak_gty  =
-    if smart then
-      match raw_gty with
-       | NCic.Appl _ 
-       | NCic.Const _ 
-       | NCic.Rel _ -> 
-            let raw_weak = 
-              perforate_small status subst metasenv context raw_gty in
-            let weak = mk_cic_term context raw_weak in
-            debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
-              Some raw_weak, Some (weak)
-       | _ -> None,None
-    else None,None
-  in
-  let global_cands, smart_global_cands =
-    match flags.candidates with
-      | Some l when (not maxd) -> l,[]
-      | Some _ 
-      | None -> 
-         let mapf s = 
-           let to_ast = function 
-             | NCic.Const r when true (*is_relevant statistics r*) -> Some (Ast.NRef r)
-       (*       | NCic.Const _ -> None  *)
-             | _ -> assert false in
-             HExtlib.filter_map 
-               to_ast (NDiscriminationTree.TermSet.elements s) in
-         let g,l = 
-           get_cands
-             (NDiscriminationTree.DiscriminationTree.retrieve_unifiables 
-                universe)
-             NDiscriminationTree.TermSet.diff 
-             NDiscriminationTree.TermSet.empty
-             raw_gty raw_weak_gty in
-           mapf g, mapf l in
-  let local_cands,smart_local_cands = 
-    let mapf s = 
-      let to_ast t =
-       let _status, t = term_of_cic_term status t context 
-       in Ast.NCic t in
-       List.map to_ast (Ncic_termSet.elements s) in
-    let g,l = 
-      get_cands
-       (fun ty -> search_in_th ty cache)
-       Ncic_termSet.diff  Ncic_termSet.empty gty weak_gty in
-      mapf g, mapf l in
-    sort_candidates status context (global_cands@local_cands),
-    sort_candidates status context (smart_global_cands@smart_local_cands)
-;; 
-
-let applicative_case depth signature status flags gty cache =
-  app_counter:= !app_counter+1; 
-  let _,_,metasenv,subst,_ = status#obj in
-  let context = ctx_of gty in
-  let tcache = cache.facts in
-  let is_prod, is_eq =   
-    let status, t = term_of_cic_term status gty context  in 
-    let t = NCicReduction.whd status subst context t in
-      match t with
-       | NCic.Prod _ -> true, false
-       | _ -> false, NCicParamod.is_equation status metasenv subst context t 
-  in
-  debug_print ~depth (lazy (string_of_bool is_eq)); 
-  (* new *)
-  let candidates, smart_candidates = 
-    get_candidates ~smart:true depth 
-      flags status tcache signature gty in 
-  let test = is_a_fact_ast status subst metasenv context in
-  let candidates_facts,candidates_other =
-    (* if the goal is an equation we avoid to apply unit equalities,
-     since superposition should take care of them; refl is an
-     exception since it prompts for convertibility *)
-    let l1,l2 = List.partition test candidates in
-    (* put the right uri *)
-    if is_eq then [Ast.Ident("refl",`Ambiguous)],l2 else l1,l2
-  in
-  let smart_candidates_facts, smart_candidates_other =
-    match flags.candidates with
-    | Some l -> [],l
-    | None ->
-        let l1,l2 = List.partition test smart_candidates in
-        if is_eq then [],l2 else l1,l2
-  in
-  let sm = if is_eq then 0 else 2 in
-  let sm1 = if flags.last then 2 else 0 in
-  let maxd = (depth + 1 = flags.maxdepth) in 
-  let try_candidates only_one sm acc candidates =
-    List.fold_left 
-      (fun elems cand ->
-         if (only_one && (elems <> [])) then elems 
-         else
-           match try_candidate (~smart:sm) 
-             flags depth status cache.unit_eq context cand with
-               | None -> elems
-               | Some x -> x::elems)
-      acc candidates
-  in 
-  (* if the goal is the last one we stop at the first fact *)
-  let elems = try_candidates flags.last sm [] candidates_facts in
-  (* now we add smart_facts *)
-  let elems = try_candidates flags.last sm elems smart_candidates_facts in
-  (* if we are at maxdepth and the goal is not a product we are done 
-     similarly, if the goal is the last one and we already found a
-     solution *)
-  if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
-  else
-    let elems = try_candidates false 2 elems candidates_other in
-    debug_print ~depth (lazy ("not facts: try smart application"));
-    try_candidates false 2 elems smart_candidates_other
-;; *)
-
 exception Found
 ;; 
 
-
-
 (* gty is supposed to be meta-closed *)
 let is_subsumed depth filter_depth status gty cache =
   if cache=[] then false else (