parameter sintax added to axiom statement

[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 62e4844997e72f73bc02ae8e0c99fecaaee7f264..44f30d278a00f69792788d3a074754804f509421 100644 (file)
--- a/helm/software/components/cic_unification/coercGraph.mli
+++ b/helm/software/components/cic_unification/coercGraph.mli
@@ -32,27 +32,25 @@ type coercion_search_result =
      (* to apply the coercion it is sufficient to unify the last coercion
         argument (that is a Meta) with the term to be coerced *)
   | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
+  | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
   | NoCoercion
-  | NotMetaClosed
-  | NotHandled of string Lazy.t
+  | NotHandled
 
 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
-
 val source_of: Cic.term -> Cic.term
 
-val generate_dot_file: unit -> string
+val generate_dot_file: Format.formatter -> unit
 
+(* given the Appl contents returns the argument of the head coercion *)
+val coerced_arg: Cic.term list -> (Cic.term * int) option
+
+(* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *)
 val meets : 
-  CoercDb.coerc_carr -> CoercDb.coerc_carr -> 
-    CoercDb.coerc_carr list
+  Cic.metasenv -> Cic.substitution -> Cic.context ->
+  bool * CoercDb.coerc_carr -> bool * CoercDb.coerc_carr -> 
+    (CoercDb.coerc_carr * Cic.metasenv * 
+      (Cic.term * Cic.term) option * (Cic.term * Cic.term) option) list