From 8bb15cf06201f98356f8676a3a1c607151c2aec6 Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 29 Jul 2011 14:25:28 +0000
Subject: Tactics: generic equality on constr replaced by eq_constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14326 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3ad89c8254..dd0541fd07 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2680,7 +2680,7 @@ let compute_scheme_signature scheme names_info ind_type_guess =
 	let is_pred n c =
 	  let hd = fst (decompose_app c) in match kind_of_term hd with
 	    | Rel q when n < q & q <= n+scheme.npredicates -> IndArg
-	    | _ when hd = indhd -> RecArg
+	    | _ when eq_constr hd indhd -> RecArg
 	    | _ -> OtherArg in
 	let rec check_branch p c = match kind_of_term c with
 	  | Prod (_,t,c) ->
-- 
cgit v1.2.3