From 5e4afc4cd404446701c5ede02041a3beec8d0975 Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 29 Jul 2011 14:27:01 +0000
Subject: Tactics: generic equality on constr replaced by eq_constr

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index dd0541fd07..1c1843a124 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2646,7 +2646,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 = ind_type_guess & not scheme.farg_in_concl -> RecArg
+	    | _ when eq_constr hd ind_type_guess & not scheme.farg_in_concl -> RecArg
 	    | _ -> OtherArg in
 	let rec check_branch p c =
 	  match kind_of_term c with
-- 
cgit v1.2.3