Fixed (yet another) nasty bug, in deep_eq this time

[helm.git] / helm / software / components / cic_unification / coercGraph.mli

diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli
index 6c6ef2b50f2089230f39eabd50db0bccbaee0736..3bc6273c34e44721dcf76ea85bfb0e16e3171db9 100644 (file)
--- a/helm/software/components/cic_unification/coercGraph.mli
+++ b/helm/software/components/cic_unification/coercGraph.mli
@@ -40,10 +40,6 @@ val look_for_coercion :
   Cic.metasenv -> Cic.substitution -> Cic.context ->
    Cic.term -> Cic.term -> coercion_search_result
 
-(* checks if term is a constant or 
- * a constant applyed that is marked with (`Class `Coercion) *)
-val is_composite: Cic.term -> bool
-
 val source_of: Cic.term -> Cic.term
 
 val generate_dot_file: unit -> string