moved "hint" from Command to Macro

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index d7096ae79deeeb40e4fbd7e9e9949b76956a29c6..e1623f3d2bbcec6387f688798e5d253adb40af0d 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -368,7 +368,6 @@ EXTEND
     | [ IDENT "fourier" ] ->
         TacticAst.Fourier loc
     | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n)
-    | [ IDENT "hint" ] -> TacticAst.Hint loc
     | [ IDENT "injection" ]; ident = IDENT ->
         TacticAst.Injection (loc, ident)
     | [ IDENT "intros" ];
@@ -480,6 +479,7 @@ EXTEND
         TacticAst.Redo (loc, int_opt steps)
     | [ IDENT "check"   ]; t = term ->
         TacticAst.Check (loc, t)
+    | [ IDENT "hint" ] -> TacticAst.Hint loc
     | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
   ]];
 

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 809c57dfeec551a0da04f9f9d468341032512007..a7b0fbeafa523dc402ab4df99cc9e93c8aefd215 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -54,7 +54,6 @@ type ('term, 'ident) tactic =
   | Fold of loc * reduction_kind * 'term
   | Fourier of loc
   | Goal of loc * int (* change current goal, argument is goal number 1-based *)
-  | Hint of loc
   | Injection of loc * 'ident
   | Intros of loc * int option * 'ident list
   | Left of loc
@@ -96,6 +95,7 @@ type 'term macro =
   | Abort of loc
   | Print of loc * string
   | Check of loc * 'term 
+  | Hint of loc
   | Quit of loc
   | Redo of loc * int option
   | Undo of loc * int option

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index 74a6a749eb245704364bb4b4f34bd3681fd1c87f..cb06a8edf6dc9d67f410fed7689a6bf6ad2e8230 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -69,7 +69,6 @@ let rec count_tactic current_size tac =
        countterm (current_size + 5) term
     | Fourier _ -> current_size + 7
     | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
-    | Hint _ -> current_size + 4
     | Injection (_, ident) -> current_size + 10 + (String.length ident)
     | Intros (_, num, idents) ->
        List.fold_left 
@@ -191,7 +190,6 @@ and big_tactic2box = function
                Box.indent(ast2astBox term)])
   | Fourier _ -> Box.Text([],"fourier")
   | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
-  | Hint _ -> Box.Text([],"hint")
   | Injection (_, ident) -> 
       Box.V([],[Box.Text([],"transitivity");
                Box.indent (Box.Text([],ident))])

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 1a28fa578004b6d0a71b3df0ceea1ab9e7a1aee2..99fc38553a49c60b7eeb8b2505511ef9701253c7 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -65,7 +65,6 @@ let rec pp_tactic = function
       sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term_ast term)
   | Goal (_, n) -> "goal " ^ string_of_int n
   | Fourier _ -> "fourier"
-  | Hint _ -> "hint"
   | Injection (_, ident) -> "injection " ^ ident
   | Intros (_, None, []) -> "intro"
   | Intros (_, num, idents) ->
@@ -112,6 +111,7 @@ let pp_search_kind = function
 let pp_macro pp_term = function 
   | Abort _ -> "Abort"
   | Check (_, term) -> sprintf "Check %s" (pp_term term)
+  | Hint _ -> "hint"
   | Redo (_, None) -> "Redo"
   | Redo (_, Some n) -> sprintf "Redo %d" n
   | Search_pat (_, kind, pat) ->