Procedural: 2 bug fix in eta expansion + 1 bug fix in pattern generation

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

diff --git a/helm/software/components/acic_procedural/proceduralTypes.mli b/helm/software/components/acic_procedural/proceduralTypes.mli
index 9fb7f30351fdfc9868ce7ed337e6638792893657..33a7e9c05c51e16a8f23b97407678daeb4a2e5fe 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.mli
+++ b/helm/software/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,11 +52,11 @@ 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
-         | Whd of count * note
-         | Change of inferred * what * note
+         | Change of inferred * what * where * pattern * note
+         | ClearBody of name * note
          | Branch of step list list * note
 
 val render_steps: