Procedural: some improvements

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

diff --git a/components/acic_procedural/proceduralTypes.mli b/components/acic_procedural/proceduralTypes.mli
index 980bc1bc1c71796fe462829b96caa0414968775d..33a7e9c05c51e16a8f23b97407678daeb4a2e5fe 100644 (file)
--- a/components/acic_procedural/proceduralTypes.mli
+++ b/components/acic_procedural/proceduralTypes.mli
@@ -43,6 +43,7 @@ type count    = int
 type note     = string
 type where    = (name * name) option
 type inferred = Cic.annterm
+type pattern  = Cic.annterm
 
 type step = Note of note 
           | Theorem of name * what * note
@@ -51,10 +52,10 @@ type step = Note of note
          | Intros of count option * name list * note
           | Cut of name * what * note
           | LetIn of name * what * note
-         | Rewrite of how * what * where * note
+         | Rewrite of how * what * where * pattern * note
          | Elim of what * using option * note
          | Apply of what * note
-         | Change of inferred * what * where * note
+         | Change of inferred * what * where * pattern * note
          | ClearBody of name * note
          | Branch of step list list * note