From a7ab0ef67114c3152920f03ae1d7bfaaf1fae290 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli 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