From 2292dd89b9b36ec8c865ab67e5291088bfcc4806 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 1 Mar 2006 17:34:36 +0000
Subject: Correction bug #842 (rename d'une hyp du contexte)

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

(limited to 'contrib/xml')

diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml
index f78df74789..dff546c948 100644
--- a/contrib/xml/proof2aproof.ml
+++ b/contrib/xml/proof2aproof.ml
@@ -117,7 +117,7 @@ let extract_open_proof sigma pf =
              (fun id ->
                 (* Section variables are in the [id] list but are not *)
                 (* lambda abstracted in the term [vl]                 *)
-                try let n = Util.list_index id vl in (n,id)
+                try let n = Logic.proof_variable_index id vl in (n,id)
 	        with Not_found -> failwith "caught")
 (*CSC: the above function must be modified such that when it is found  *)
 (*CSC: it becomes a Rel; otherwise a Var. Then it can be already used  *)
-- 
cgit v1.2.3