elim tactic: now takes a pattern instead of just a term

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

diff --git a/components/acic_procedural/proceduralTypes.mli b/components/acic_procedural/proceduralTypes.mli
index 33a7e9c05c51e16a8f23b97407678daeb4a2e5fe..97ca7fdbb98bd21518673169db3d2d97fcd4f2f0 100644 (file)
--- a/components/acic_procedural/proceduralTypes.mli
+++ b/components/acic_procedural/proceduralTypes.mli
@@ -53,7 +53,7 @@ type step = Note of note
           | Cut of name * what * note
           | LetIn of name * what * note
          | Rewrite of how * what * where * pattern * note
-         | Elim of what * using option * note
+         | Elim of what * using option * pattern * note
          | Apply of what * note
          | Change of inferred * what * where * pattern * note
          | ClearBody of name * note