From ef42739eadeb6ec3fc98b5beaa13bd859de44d15 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 23 Oct 2013 22:17:11 +0000
Subject: cList.index is now cList.index_f, same for index0

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

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 13e422b54f..b72bb02641 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -114,7 +114,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
         [([_],_,_)], None -> 1
       | _, Some x ->
           let ids = List.map snd (List.flatten (List.map pi1 bl)) in
-          (try List.index (snd x) ids
+          (try List.index Names.Name.equal (snd x) ids
           with Not_found -> error "No such fix variable.")
       | _ -> error "Cannot guess decreasing argument of fix." in
   (id,n,CProdN(loc,bl,ty))
-- 
cgit v1.2.3