unification+pullback fix. It used to saturate a coercion (generating new metas)

[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 abc94688c5a6b27897ca1c63b2fc8a1946e45efd..6c6ef2b50f2089230f39eabd50db0bccbaee0736 100644 (file)
--- a/helm/software/components/cic_unification/coercGraph.mli
+++ b/helm/software/components/cic_unification/coercGraph.mli
@@ -54,7 +54,7 @@ val coerced_arg: Cic.term list -> (Cic.term * int) option
 (* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *)
 val meets : 
   Cic.metasenv -> Cic.substitution -> Cic.context ->
-  CoercDb.coerc_carr -> CoercDb.coerc_carr -> 
+  bool * CoercDb.coerc_carr -> bool * CoercDb.coerc_carr -> 
     (CoercDb.coerc_carr * Cic.metasenv * 
       (Cic.term * Cic.term) option * (Cic.term * Cic.term) option) list