From eacab552644acdaf9922d831a09e8318f9c96980 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 23 Jun 2006 10:17:14 +0000
Subject: Suite utilisation hyp au lieu ident: donne la localisationn

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8979 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/extratactics.ml4 | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 41b79fefba..6fcf728331 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -46,10 +46,6 @@ let pr_by_arg_tac _prc _prlc prtac opt_c =
     | None -> mt ()
     | Some t -> spc () ++ hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
 
-(* Julien Forest: on voudrait pouvoir passer la loc mais je 
-n'ai pas reussi 
-*)
-
 let pr_in_hyp = function
   | None -> mt ()
   | Some id -> spc () ++ hov 2 (str "in" ++ spc () ++ Nameops.pr_id id)
-- 
cgit v1.2.3