From c05b36907ed2bf71300dffc2f4a6602dc1288045 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 10 Jun 2005 15:45:35 +0000 Subject: [PATCH] Got rid of a few warnings. --- helm/ocaml/cic_transformations/tacticAst2Box.ml | 6 ++++-- helm/ocaml/cic_transformations/tacticAstPp.ml | 3 +++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index d2df977fa..4f1c27f47 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -77,7 +77,8 @@ let rec count_tactic current_size tac = | Left _ -> current_size + 4 | LetIn (_, term, ident) -> countterm (current_size + 5 + String.length ident) term - | Reduce _ -> assert false (* TODO *) + | Reduce _ + | ReduceAt _ -> assert false (* TODO *) | Reflexivity _ -> current_size + 11 | Replace (_, t1, t2) -> let size1 = countterm (current_size + 14) t1 in (* replace, with *) @@ -212,7 +213,8 @@ and big_tactic2box = function Box.smallskip; Box.Text([],"=")]); Box.indent (ast2astBox term)]) - | Reduce _ -> assert false (* TODO *) + | Reduce _ + | ReduceAt _ -> assert false (* TODO *) | Reflexivity _ -> Box.Text([],"reflexivity") | Replace (_, t1, t2) -> Box.V([], diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 9882aa0e9..822618eb4 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -85,6 +85,9 @@ let rec pp_tactic = function | Reduce (_, kind, Some (terms, `Everywhere)) -> sprintf "%s in hyp %s" (pp_reduction_kind kind) (String.concat ", " (List.map pp_term_ast terms)) + | ReduceAt (_, kind, id, term) -> + sprintf "%s %s at %s" (pp_reduction_kind kind) id + (pp_term_ast term) | Reflexivity _ -> "reflexivity" | Replace (_, t1, t2) -> sprintf "replace %s with %s" (pp_term_ast t1) (pp_term_ast t2) -- 2.39.2