Generation of inductive and inversion principles for mutual

[helm.git] / components / library / librarySync.mli

diff --git a/components/library/librarySync.mli b/components/library/librarySync.mli
index b29a0aa0342b33442b57272f144556029cc24d46..61e2b2515ae9ba36837b142427cfd508b12014a5 100644 (file)
--- a/components/library/librarySync.mli
+++ b/components/library/librarySync.mli
@@ -26,7 +26,7 @@
 exception AlreadyDefined of UriManager.uri
 
 (* this is a pointer to the function which builds the inversion principle *)
-val build_inversion_principle: (UriManager.uri-> Cic.obj -> (UriManager.uri * Cic.obj) option) ref
+val build_inversion_principle: (UriManager.uri-> Cic.obj -> (UriManager.uri * Cic.obj) list) ref
 
 (* adds an object to the library together with all auxiliary lemmas on it *)
 (* (e.g. elimination principles, projections, etc.)                       *)