Cic.term and Cic.obj unused!

[helm.git] / matita / components / grafite_engine / grafiteTypes.ml

diff --git a/matita/components/grafite_engine/grafiteTypes.ml b/matita/components/grafite_engine/grafiteTypes.ml
index 7f264d6fa0a623479e6eed5d0b65bdf8139b295f..d68331fecfb1603f9aef86362ed6b0b5605b797b 100644 (file)
--- a/matita/components/grafite_engine/grafiteTypes.ml
+++ b/matita/components/grafite_engine/grafiteTypes.ml
@@ -55,19 +55,7 @@ class status = fun (b : string) ->
 
 let add_moo_content cmds status =
   let content = status#moo_content_rev in
-  let content' =
-    List.fold_right
-      (fun cmd acc ->
-(*         prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
-        match cmd with
-        | GrafiteAst.Default _ 
-        | GrafiteAst.Index _
-        | GrafiteAst.Coercion _ ->
-            if List.mem cmd content then acc
-            else cmd :: acc
-        | _ -> cmd :: acc)
-      cmds content
-  in
+  let content' = cmds@content in
 (*   prerr_endline ("new moo content: " ^ String.concat " " (List.map
     GrafiteAstPp.pp_command content')); *)
    status#set_moo_content_rev content'