X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=4ab7412d832c60f4e0c0c0aab339e5ef9f2a652e;hb=1bd6b7d2637d765f11ddbd1218d63474e9d0c63b;hp=6b341f77c314a581e130e7e9e7f55ad712821334;hpb=7233348f05485c2ee317df9c3407cf1ce7e56927;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 6b341f77c..4ab7412d8 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -336,14 +336,14 @@ let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) =
  let after = ProofEngineTypes.goals_of_proof proof in
  let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
  let proof, opened_goals = 
-  let uri, metasenv_after_tactic, _subst, t, ty, attrs = proof in
+  let uri, metasenv_after_tactic, subst, t, ty, attrs = proof in
   let reordered_metasenv, opened_goals = 
     reorder_metasenv
      starting_metasenv
      metasenv_after_refinement metasenv_after_tactic
      opened goal always_opens_a_goal
   in
-  let proof' = uri, reordered_metasenv, _subst, t, ty, attrs in
+  let proof' = uri, reordered_metasenv, [], t, ty, attrs in
   proof', opened_goals
  in
  let incomplete_proof =
@@ -758,12 +758,13 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
              else
               let obj =
 prerr_endline "CSC: here we should fix the height!!!";
-               uri,height,[],[],NTacStatus.apply_subst_obj subst obj
+               uri,height,[],[],
+                NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst) obj
               in
                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;
@@ -784,12 +785,13 @@ prerr_endline "CSC: here we should fix the height!!!";
           (* CSC: cut&paste code from NQed *)
           let obj =
 prerr_endline "CSC: here we should fix the height!!!";
-           uri,height,[],[],NTacStatus.apply_subst_obj nsubst nobj
+           uri,height,[],[],
+            NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst nsubst) nobj
           in
            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 +799,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 +890,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