1 files changed, 22 insertions, 0 deletions
diff --git a/contrib/subtac/Tactics.v b/contrib/subtac/Tactics.v
new file mode 100644
index 000000000..25d8d8319
--- /dev/null
+++ b/contrib/subtac/Tactics.v
@@ -0,0 +1,22 @@
+Ltac induction_with_subterm c H :=
+  let x := fresh "x" in
+  let y := fresh "y" in
+  (set(x := c) ; assert(y:x = c) by reflexivity ;
+  rewrite <- y in H ; 
+  induction H ; subst).
+
+Ltac induction_on_subterm c :=
+  let x := fresh "x" in
+  let y := fresh "y" in
+  (set(x := c) ; assert(y:x = c) by reflexivity ; clearbody x ; induction x ; inversion y ; try subst ; 
+  clear y).
+
+Ltac induction_with_subterms c c' H :=
+  let x := fresh "x" in
+  let y := fresh "y" in
+  let z := fresh "z" in
+  let w := fresh "w" in
+  (set(x := c) ; assert(y:x = c) by reflexivity ;
+  set(z := c') ; assert(w:z = c') by reflexivity ;
+  rewrite <- y in H ; rewrite <- w in H ; 
+  induction H ; subst).