- cic_exportation, cic_acic, acic_content (only parts related to acic)

[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 33ec596f55fcb4c4dcc2327b6fc54cc762180788..8e925db628b08b9082fb271a7ebe63f69708f1b2 100644 (file)
--- a/matita/components/grafite_engine/grafiteSync.ml
+++ b/matita/components/grafite_engine/grafiteSync.ml
@@ -55,23 +55,6 @@ let uris_for_inductive_type uri obj =
     | _ -> [uri] 
 ;;
 
-let is_equational_fact ty =
-  let rec aux ctx t = 
-    match CicReduction.whd ctx t with 
-    | Cic.Prod (name,src,tgt) ->
-        let s,u = 
-          CicTypeChecker.type_of_aux' [] ctx src CicUniv.oblivion_ugraph
-        in
-        if fst (CicReduction.are_convertible ctx s (Cic.Sort Cic.Prop) u) then
-          false
-        else
-          aux (Some (name,Cic.Decl src)::ctx) tgt
-    | Cic.Appl [ Cic.MutInd (u,_,_) ; _; _; _] -> LibraryObjects.is_eq_URI u
-    | _ -> false
-  in 
-    aux [] ty
-;;
-    
 let add_coercion ~pack_coercion_obj ~add_composites status uri arity
  saturations baseuri
 =