weakly/strictly positive checks relaxed to allow metavariables that are not

[helm.git] / helm / software / components / library / coercDb.mli

diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli
index 83e61dbfba2f708097e12e7b04dcef6e6ffda710..59c07f447acd3796130a16b2fc238b2e52969407 100644 (file)
--- a/helm/software/components/library/coercDb.mli
+++ b/helm/software/components/library/coercDb.mli
@@ -37,15 +37,15 @@ val string_of_carr: coerc_carr -> string
 (* takes a term in whnf ~delta:false and a desired ariety *)
 val coerc_carr_of_term: Cic.term -> int -> coerc_carr 
 
-val to_list:
-  unit -> 
-    (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list
-
 type coerc_db
 val empty_coerc_db : coerc_db
 val dump: unit -> coerc_db
 val restore: coerc_db -> unit
 
+val to_list:
+  coerc_db -> 
+    (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list
+
 (* src carr, tgt carr, uri, saturations, coerced position 
  * invariant:
  *   if the constant pointed by uri has n argments