Multi-user matita: changed the status object to include a ``user'' method

[helm.git] / matitaB / components / ng_tactics / nTactics.ml

diff --git a/matitaB/components/ng_tactics/nTactics.ml b/matitaB/components/ng_tactics/nTactics.ml
index aecc88e1f5e9ff0b310487fe79122a07125a3def..889b8b309c76ab528d4bc8b8a2370a24c869b26b 100644 (file)
--- a/matitaB/components/ng_tactics/nTactics.ml
+++ b/matitaB/components/ng_tactics/nTactics.ml
@@ -205,9 +205,10 @@ let compare_statuses ~past ~present =
 (* CSC: potential bug here: the new methods still use the instance variables
    of the old status and not the instance variables of the new one *)
 let change_stack_type (status : 'a #NTacStatus.status) (stack: 'b) : 'b NTacStatus.status =
+ let uid = status#user in
  let o =
   object
-   inherit ['b] NTacStatus.status status#obj stack
+   inherit ['b] NTacStatus.status uid status#obj stack
    method ppterm = status#ppterm
    method ppcontext = status#ppcontext
    method ppsubst = status#ppsubst