From ef2947e49ef51f8e4f75ad2226df473bc53ee5c5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 15 Apr 2001 00:53:39 +0000
Subject: Bug affichage d'implicites pour les vars liees

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1593 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/termast.ml | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/parsing/termast.ml b/parsing/termast.ml
index 34b6cf65b6..7b7ad5848c 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -184,14 +184,6 @@ let rec ast_of_raw = function
       (match f with 
 	 | REvar (_,ev) -> ast_of_existential_ref ev (* we drop args *)
 	 | RRef (_,ref) -> ast_of_app (implicits_of_global ref) astf astargs
-
-	 | RVar (_,id) ->
-	     let imp =
-	       try 
-		 let ref = Nametab.locate (make_qualid [] id) in
-		 implicits_of_global ref
-	       with Not_found -> [] in
-	     ast_of_app imp astf astargs
 	 | _       -> ast_of_app [] astf astargs)
 
   | RProd (_,Anonymous,t,c) ->
-- 
cgit v1.2.3