From 7e7ce7bb6b95e9bd10dc180671ba7512ff2537dd Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 28 Apr 2005 13:32:42 +0000
Subject: [PATCH] moved "hint" from Command to Macro

---
 helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 2 +-
 helm/ocaml/cic_transformations/tacticAst.ml        | 2 +-
 helm/ocaml/cic_transformations/tacticAst2Box.ml    | 2 --
 helm/ocaml/cic_transformations/tacticAstPp.ml      | 2 +-
 4 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index d7096ae79..e1623f3d2 100644
--- 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 809c57dfe..a7b0fbeaf 100644
--- 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 74a6a749e..cb06a8edf 100644
--- 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 1a28fa578..99fc38553 100644
--- 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) ->
-- 
2.39.2