From 0225d6e1fbf24f32908bb3c78cd4ce54c994a1ca Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 2 Jan 2007 16:18:54 +0000
Subject: Add f_equal case for 6 arguments.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9469 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Tactics.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 9a2856128a..ab3754b34f 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -44,8 +44,10 @@ Ltac f_equal :=
       cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]
    | |- ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d'=> 
       cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]
-  | |- ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e'=> 
+   | |- ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e'=> 
       cut (e=e');[cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]|r]
+   | |- ?f ?a ?b ?c ?d ?e ?f= ?f' ?a' ?b' ?c' ?d' ?e' ?f' => 
+      cut (f=f');[cut (e=e');[cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]|r]|r]
    | _ => idtac
   end.
 
-- 
cgit v1.2.3