nasty change in the lexer/parser:

[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 037a36f38ca164790ba9b5af23f75c88c752d841..a3748f3cd1b259c0a7dd2b19d063dbb3b9b7fed0 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -629,6 +629,17 @@ let eval_ng_tac (text, prefix_len, tac) =
      NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what)
       ~where:(text,prefix_len,where)
 ;;
+      
+let subst_metasenv_and_fix_names s =
+  let u,h,metasenv, subst,o = s.NTacStatus.istatus.NTacStatus.pstatus in
+  let o = 
+    NCicUntrusted.map_obj_kind ~skip_body:true 
+     (NCicUntrusted.apply_subst subst []) o
+  in
+  { s with NTacStatus.istatus =
+     { s.NTacStatus.istatus with NTacStatus.pstatus =
+        u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o}}
+;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status
 (text,prefix_len,cmd) ->
@@ -766,7 +777,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
               let obj =
 prerr_endline "CSC: here we should fix the height!!!";
                (uri,height,[],[],
-                NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst)
+                NCicUntrusted.map_obj_kind 
+                  (NCicUntrusted.apply_subst subst [])
                  obj) in
               NCicTypeChecker.typecheck_obj obj;
               NCicLibrary.add_obj uri obj;
@@ -806,9 +818,10 @@ prerr_endline "CSC: here we should fix the height!!!";
       { status with
          GrafiteTypes.ng_status = 
           GrafiteTypes.ProofMode
-           { NTacStatus.gstatus = ninitial_stack; 
-             istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}}
-           }
+           (subst_metasenv_and_fix_names
+            { NTacStatus.gstatus = ninitial_stack; 
+             istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}})
+             }
      in
      (match nmenv with
          [] ->
@@ -909,6 +922,7 @@ prerr_endline "CSC: here we should fix the height!!!";
       | GrafiteTypes.CommandMode _ -> assert false
       | GrafiteTypes.ProofMode nstatus ->
          let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
+         let nstatus = subst_metasenv_and_fix_names 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 },