This commit patches the environment and the library so that their status is

[helm.git] / matitaB / components / grafite_engine / grafiteTypes.ml

diff --git a/matitaB/components/grafite_engine/grafiteTypes.ml b/matitaB/components/grafite_engine/grafiteTypes.ml
index 5b34158c41a643bbd556a6b811db8bd6d5cae19c..f4ec3309c27976ff7f0510a2db466da7593329d7 100644 (file)
--- a/matitaB/components/grafite_engine/grafiteTypes.ml
+++ b/matitaB/components/grafite_engine/grafiteTypes.ml
@@ -39,7 +39,7 @@ class virtual status = fun (uid : string option) (b : string) ->
   object
    (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
    inherit ([Continuationals.Stack.t] NTacStatus.status uid fake_obj (Continuationals.Stack.empty))
-   inherit NCicLibrary.dumpable_status
+   inherit NCicLibrary.dumpable_status uid
    inherit NCicLibrary.status uid
    inherit GrafiteDisambiguate.status uid
    inherit GrafiteParser.status uid