From 67f5c70a480c95cfb819fc68439781b5e5e95794 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 14 Dec 2012 15:56:25 +0000
Subject: Modulification of identifier

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

(limited to 'proofs/refiner.ml')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 704dd9887..c83d5ca7a 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -204,7 +204,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
     List.fold_left
     (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
       ^ (List.fold_left
-	   (fun acc (nm,_,_) -> (Names.string_of_id nm) ^ " " ^ acc)
+	   (fun acc (nm,_,_) -> (Names.Id.to_string nm) ^ " " ^ acc)
 	   "" lh))
     "" newhyps in
   pp (str (emacs_str "<infoH>")
-- 
cgit v1.2.3