Procedural : some improvements

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

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index 95fdc6e562d6c8e281c937509dd8b57d57431ab9..1d8bbbc21109120da4cd9f27c21a22abcff6a5e6 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/components/acic_procedural/proceduralTypes.ml
@@ -68,13 +68,14 @@ let is_atomic = function
 
 (****************************************************************************)
 
-type name  = string
-type what  = Cic.annterm
-type how   = bool
-type using = Cic.annterm
-type count = int
-type note  = string
-type where = (name * name) option
+type name     = string
+type what     = Cic.annterm
+type how      = bool
+type using    = Cic.annterm
+type count    = int
+type note     = string
+type where    = (name * name) option
+type inferred = Cic.annterm
 
 type step = Note of note 
           | Theorem of name * what * note
@@ -87,6 +88,7 @@ type step = Note of note
          | Elim of what * using option * note
          | Apply of what * note
          | Whd of count * note
+         | Change of inferred * what * note 
          | Branch of step list list * note
 
 (* annterm constructors *****************************************************)
@@ -149,6 +151,11 @@ let mk_whd i =
    let tactic = G.Reduce (floc, `Whd, pattern) in
    mk_tactic tactic
 
+let mk_change t =
+   let pattern = None, [], Some hole in
+   let tactic = G.Change (floc, pattern, t) in
+   mk_tactic tactic
+
 let mk_dot = G.Executable (floc, G.Tactical (floc, G.Dot floc, None))
 
 let mk_sc = G.Executable (floc, G.Tactical (floc, G.Semicolon floc, None))
@@ -164,7 +171,7 @@ let mk_vb = G.Executable (floc, G.Tactical (floc, G.Shift floc, None))
 let rec render_step sep a = function
    | Note s               -> mk_note s :: a
    | Theorem (n, t, s)    -> mk_note s :: mk_theorem n t :: a 
-   | Qed s                -> mk_note s :: mk_qed :: a
+   | Qed s                -> (* mk_note s :: *) mk_qed :: a
    | Id s                 -> mk_note s :: cont sep (mk_id :: a)
    | Intros (c, ns, s)    -> mk_note s :: cont sep (mk_intros c ns :: a)
    | Cut (n, t, s)        -> mk_note s :: cont sep (mk_cut n t :: a)
@@ -173,6 +180,7 @@ let rec render_step sep a = function
    | 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, _, s)     -> mk_note s :: cont sep (mk_change t :: a)
    | Branch ([], s)       -> a
    | Branch ([ps], s)     -> render_steps sep a ps
    | Branch (pss, s)      ->