Moving centralised discharge into dispatched discharge_function; required to delay some computation from before to after caching time + various simplifications and uniformisations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 0 deletions

diff --git a/library/libobject.mli b/library/libobject.mli
index 37447ffbe..3d60e48ad 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -70,6 +70,7 @@ type 'a object_declaration = {
   open_function : int -> object_name * 'a -> unit;
   classify_function : object_name * 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
+  discharge_function : object_name * 'a -> 'a option;
   export_function : 'a -> 'a option }
 
 (* The default object is a "Keep" object with empty methods. 
@@ -103,4 +104,5 @@ val open_object : int -> object_name * obj -> unit
 val subst_object : object_name * substitution * obj -> obj
 val classify_object : object_name * obj -> obj substitutivity
 val export_object : obj -> obj option
+val discharge_object : object_name * obj -> obj option
 val relax : bool -> unit