some improvements

[helm.git] / components / acic_procedural / proceduralTypes.ml

diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml
index b81a7c3dead0ebe02105c854bf45706e133b91bc..6aa769b03aa11ec4c209b3b5f60e0e0a1b3ddb68 100644 (file)
--- a/components/acic_procedural/proceduralTypes.ml
+++ b/components/acic_procedural/proceduralTypes.ml
@@ -87,7 +87,6 @@ type step = Note of note
          | Rewrite of how * what * where * note
          | Elim of what * using option * note
          | Apply of what * note
-         | Whd of count * note
          | Change of inferred * what * where * note 
          | ClearBody of name * note
          | Branch of step list list * note
@@ -147,11 +146,6 @@ let mk_apply t =
    let tactic = G.Apply (floc, t) in
    mk_tactic tactic
 
-let mk_whd i =
-   let pattern = None, [], Some hole in
-   let tactic = G.Reduce (floc, `Whd, pattern) in
-   mk_tactic tactic
-
 let mk_change t where =
    let pattern = match where with
       | None              -> None, [], Some hole
@@ -187,7 +181,6 @@ let rec render_step sep a = function
    | Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a)
    | Elim (t, xu, s)      -> mk_note s :: cont sep (mk_elim t xu :: a)
    | Apply (t, s)         -> mk_note s :: cont sep (mk_apply t :: a)
-   | Whd (c, s)           -> mk_note s :: cont sep (mk_whd c :: a)
    | Change (t, _, w, s)  -> mk_note s :: cont sep (mk_change t w :: a)
    | ClearBody (n, s)     -> mk_note s :: cont sep (mk_clearbody n :: a)
    | Branch ([], s)       -> a