GrafiteAst.Print (unused) removed.

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 6c6b3786ff88af760114f1e1157d09209682f5be..03b67ade37c67d68ed63d4877aaaa7b12a1734ec 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -104,7 +104,6 @@ type 'term macro =
   | WLocate of loc * string
   | WElim of loc * 'term
   (* real macros *)
-  | Print of loc * string
   | Check of loc * 'term 
   | Hint of loc
   | Quit of loc

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index c5bbe8f19fb2c0a940fede00c1c974e9af9afa80..55736e862e2cba8aa5ee548a823691af3f7810aa 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -182,7 +182,6 @@ let pp_macro ~term_pp =
   (* real macros *)
   | Check (_, term) -> sprintf "Check %s" (term_pp term)
   | Hint _ -> "hint"
-  | Print (_, name) -> sprintf "Print \"%s\"" name
   | Quit _ -> "Quit"
 
 let pp_associativity = function

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 396d169e79d0c6698e35f1d1e8665365de80cddb..4ced7a0afdd04e484836fc142195c70d2d597baa 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -326,5 +326,4 @@ let disambiguate_macro
    | GrafiteAst.Hint _
    | GrafiteAst.WLocate _ as macro ->
       metasenv,macro
-   | GrafiteAst.Quit _
-   | GrafiteAst.Print _ -> assert false
+   | GrafiteAst.Quit _ -> assert false

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 1c85b567d48feb17d98064632c60718f4531f15d..834cbcf410f34b9f31379357057526ddceaf62d5 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -362,7 +362,6 @@ EXTEND
         GrafiteAst.WElim (loc, t)
     | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> 
         GrafiteAst.WHint (loc,t)
-    | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name)
     ]
   ];
   alias_spec: [

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index a6842d832e2076251a7a14fdf82631b51e11d319..91182d6ad44aa1aa0ed0dac991d101889eb82035 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -290,7 +290,6 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
       [], parsed_text_length
   (* TODO *)
   | TA.Quit _ -> failwith "not implemented"
-  | TA.Print (_,kind) -> failwith "not implemented"
                                 
 and eval_executable include_paths (buffer : GText.buffer) guistuff
 lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt