The backward compatible management of aliases for NG is now fully completed.

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 6b341f77c314a581e130e7e9e7f55ad712821334..5caafb67b89cb2de2467d6b2a0d645f834e5015a 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -763,7 +763,7 @@ prerr_endline "CSC: here we should fix the height!!!";
                NCicLibrary.add_obj uri obj;
                {status with 
                  GrafiteTypes.ng_status = 
-                  GrafiteTypes.CommandMode lexicon_status },`Old []
+                  GrafiteTypes.CommandMode lexicon_status },`New [uri]
        | _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
   | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> 
      Setoids.add_relation id a aeq refl sym trans;
@@ -789,7 +789,7 @@ prerr_endline "CSC: here we should fix the height!!!";
            NCicLibrary.add_obj uri obj;
            {status with 
              GrafiteTypes.ng_status=GrafiteTypes.CommandMode lexicon_status },
-           `Old []
+           `New [uri]
       | _ ->
         let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
         { status with
@@ -797,7 +797,7 @@ prerr_endline "CSC: here we should fix the height!!!";
             GrafiteTypes.ProofMode
              { NTacStatus.gstatus = ninitial_stack; 
                istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}}
-             },`Old [])
+             },`New [])
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with
@@ -888,13 +888,14 @@ prerr_endline "CSC: here we should fix the height!!!";
       eval_tactical status
        (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
   | GrafiteAst.NTactic (_(*loc*), tac, punct) ->
-      (match  status.GrafiteTypes.ng_status with
+      (match status.GrafiteTypes.ng_status with
       | GrafiteTypes.CommandMode _ -> assert false
       | GrafiteTypes.ProofMode nstatus ->
          let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
          let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
          NTacStatus.pp_tac_status nstatus;
-         { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, `Old [])
+         { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
+         `New [])
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
      let status = 
       eval_tactical status