X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=5086eb845c6424574c565f8471ecc96b216bac14;hb=52d6d0a1d971e61fef9cfded716d319db5782f8f;hp=54850f1126b707ca0d765809fea7573d0fe4b0e9;hpb=0e93127aaf63e2312c214a0f8fbbc58a6cd129b7;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 54850f112..5086eb845 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -663,6 +663,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
             | _ -> status)
          else
           status in
+        (* purge tinycals stack *)
+        let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
+        let status = status#set_stack ninitial_stack in
 (*
 	  try 
 	    index_eq uri status