modifications to make matita behave reasonably, removed some useless windows

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

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 766408c13f5c25b4e3f3508f79fa1673d9b97cce..dfe0c019f4833a06d2cf8fe309249455473b2ff5 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -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