more fixes to the cleanu phase

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

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 766408c13f5c25b4e3f3508f79fa1673d9b97cce..409c0921aeb3f41b1876511fb95d2a2100921527 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -681,7 +681,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      status,[]
   | GrafiteAst.Print (_,"proofterm") ->
       let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in
-      print_endline (Auto.pp_proofterm p);
+      prerr_endline (Auto.pp_proofterm p);
       status,[]
   | GrafiteAst.Print (_,_) -> status,[]
   | GrafiteAst.Qed loc ->
@@ -711,8 +711,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
   | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> 
      Setoids.add_relation id a aeq refl sym trans;
      status, [] (*CSC: TO BE FIXED *)
-  | GrafiteAst.Set (loc, name, value) -> 
-      GrafiteTypes.set_option status name value,[]
+  | GrafiteAst.Set (loc, name, value) -> status, []
+(*       GrafiteTypes.set_option status name value,[] *)
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with