moved "hint" from Command to Macro

[helm.git] / helm / ocaml / cic_transformations / tacticAst.ml

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