acic_procedural and tactics removed

[helm.git] / matita / components / grafite_engine / grafiteSync.ml

diff --git a/matita/components/grafite_engine/grafiteSync.ml b/matita/components/grafite_engine/grafiteSync.ml
index 47744f66e0332e962b2feace6b5f42cb0399a8df..33ec596f55fcb4c4dcc2327b6fc54cc762180788 100644 (file)
--- a/matita/components/grafite_engine/grafiteSync.ml
+++ b/matita/components/grafite_engine/grafiteSync.ml
@@ -72,70 +72,6 @@ let is_equational_fact ty =
     aux [] ty
 ;;
     
-let add_obj ~pack_coercion_obj uri obj status =
- let lemmas = LibrarySync.add_obj ~pack_coercion_obj uri obj in
- let add_to_universe (automation_cache,status) uri =
-   let term = CicUtil.term_of_uri uri in
-   let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in
-   let tkeys = Universe.keys [] ty in
-   let universe = automation_cache.AutomationCache.univ in
-   let universe, index_cmd = 
-     List.fold_left 
-       (fun (universe,acc) key -> 
-         let cands = Universe.get_candidates universe key in
-         let tys = 
-           List.map
-              (fun t -> 
-                 let ty, _ = 
-                   CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph
-                 in
-                   ty)
-              cands
-         in
-         if List.for_all 
-              (fun cty -> 
-                 not (fst(CicReduction.are_convertible [] ty cty
-                 CicUniv.oblivion_ugraph))) tys 
-        then
-           Universe.index universe key term,
-           GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri)::acc
-         else
-           universe, acc)
-       (universe,[]) tkeys
-   in
-   let is_equational = is_equational_fact ty in
-   let select_cmd = 
-      if is_equational then
-       [ GrafiteAst.Select(HExtlib.dummy_floc,uri) ]
-      else
-       []
-   in
-   let automation_cache = 
-     if is_equational then
-        AutomationCache.add_term_to_active automation_cache [] [] [] term None
-     else
-        automation_cache
-   in
-   let automation_cache = 
-     { automation_cache with AutomationCache.univ = universe }  in
-   let status = GrafiteTypes.add_moo_content index_cmd status in
-   let status = GrafiteTypes.add_moo_content select_cmd status in
-   (automation_cache,status)
- in
- let uris_to_index = 
-   if is_a_variant obj then []
-   else (uris_for_inductive_type uri obj) @ lemmas 
- in
- let automation_cache,status =
-   List.fold_left add_to_universe 
-     (status#automation_cache,status) 
-     uris_to_index 
- in
-  (status
-    #set_objects (uri :: lemmas @ status#objects))
-    #set_automation_cache automation_cache,
-  lemmas
-
 let add_coercion ~pack_coercion_obj ~add_composites status uri arity
  saturations baseuri
 =