PrimitiveTactics: intros _ now aveilable

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

diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml
index a1d120f807a161ac7aeb472e17d5518a63f28dcf..bc725d118f1124d3d2d3adf22492677a20a797cc 100644 (file)
--- a/components/acic_procedural/proceduralTypes.ml
+++ b/components/acic_procedural/proceduralTypes.ml
@@ -51,13 +51,14 @@ let list_init f i =
 
 (****************************************************************************)
 
-type name     = string
+type name     = string option
+type hyp      = string
 type what     = Cic.annterm
 type how      = bool
 type using    = Cic.annterm
 type count    = int
 type note     = string
-type where    = (name * name) option
+type where    = (hyp * name) option
 type inferred = Cic.annterm
 type pattern  = Cic.annterm
 
@@ -72,7 +73,8 @@ type step = Note of note
          | Elim of what * using option * pattern * note
          | Apply of what * note
          | Change of inferred * what * where * pattern * note 
-         | ClearBody of name * note
+         | Clear of hyp list * note
+         | ClearBody of hyp * note
          | Branch of step list list * note
 
 (* annterm constructors *****************************************************)
@@ -94,7 +96,8 @@ let mk_notenote str a =
 let mk_thnote str a =
    if str = "" then a else mk_note "" :: mk_note str :: a
 
-let mk_theorem name t = 
+let mk_theorem name t =
+   let name = match name with Some name -> name | None -> assert false in
    let obj = N.Theorem (`Theorem, name, t, None) in
    G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
 
@@ -111,15 +114,17 @@ let mk_id punctation =
    let tactic = G.IdTac floc in
    mk_tactic tactic punctation
 
-let mk_intros xi ids punctation =
-   let tactic = G.Intros (floc, xi, ids) in
+let mk_intros xi xids punctation =
+   let tactic = G.Intros (floc, (xi, xids)) in
    mk_tactic tactic punctation
 
 let mk_cut name what punctation =
+   let name = match name with Some name -> name | None -> assert false in
    let tactic = G.Cut (floc, Some name, what) in
    mk_tactic tactic punctation
 
 let mk_letin name what punctation =
+   let name = match name with Some name -> name | None -> assert false in
    let tactic = G.LetIn (floc, what, name) in
    mk_tactic tactic punctation
 
@@ -134,7 +139,7 @@ let mk_rewrite direction what where pattern punctation =
 
 let mk_elim what using pattern punctation =
    let pattern = None, [], Some pattern in
-   let tactic = G.Elim (floc, what, using, pattern, Some 0, []) in
+   let tactic = G.Elim (floc, what, using, pattern, (Some 0, [])) in
    mk_tactic tactic punctation
 
 let mk_apply t punctation =
@@ -149,6 +154,10 @@ let mk_change t where pattern punctation =
    let tactic = G.Change (floc, pattern, t) in
    mk_tactic tactic punctation
 
+let mk_clear ids punctation =
+   let tactic = G.Clear (floc, ids) in
+   mk_tactic tactic punctation
+
 let mk_clearbody id punctation =
    let tactic = G.ClearBody (floc, id) in
    mk_tactic tactic punctation
@@ -179,6 +188,7 @@ let rec render_step sep a = function
    | Elim (t, xu, e, s)      -> mk_elim t xu e sep :: mk_tacnote s a
    | Apply (t, s)            -> mk_apply t sep :: mk_tacnote s a
    | Change (t, _, w, e, s)  -> mk_change t w e sep :: mk_tacnote s a
+   | Clear (ns, s)           -> mk_clear ns sep :: mk_tacnote s a
    | ClearBody (n, s)        -> mk_clearbody n sep :: mk_tacnote s a
    | Branch ([], s)          -> a
    | Branch ([ps], s)        -> render_steps sep a ps