From a7ab0ef67114c3152920f03ae1d7bfaaf1fae290 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 22 Oct 2004 13:03:07 +0000
Subject: [PATCH] added Hint "tactic"

---
 helm/ocaml/cic_transformations/tacticAst.ml   | 1 +
 helm/ocaml/cic_transformations/tacticAstPp.ml | 1 +
 2 files changed, 2 insertions(+)

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 05e8458f8..5bc446298 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -49,6 +49,7 @@ type ('term, 'ident) tactic =
   | Exists
   | Fold of reduction_kind * 'term
   | Fourier
+  | Hint
   | Injection of 'ident
   | Intros of int option * 'ident list
   | Left
diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 75977662b..e98e7acfe 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -59,6 +59,7 @@ let rec pp_tactic = function
   | Fold (kind, term) ->
       sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term term)
   | Fourier -> "fourier"
+  | Hint -> "hint"
   | Injection ident -> "injection " ^ ident
   | Intros (num, idents) ->
       sprintf "intros%s%s"
-- 
2.39.2