Procedural: explicit flavour specification for constants is now working

[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 1a3be89f38efb20bc13b77b3752d232b4c8992b7..abc94688c5a6b27897ca1c63b2fc8a1946e45efd 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
 
-val look_for_coercion' :
-  Cic.metasenv -> Cic.substitution -> Cic.context ->
-   CoercDb.coerc_carr -> CoercDb.coerc_carr -> 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