From 22cb4d34d7f67eb98c737b076a4ecbbf800bdc55 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Tue, 7 Dec 2004 17:41:10 +0000
Subject: The type Pattern.constr_label was isomorphic to
 Libnames.global_reference.

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

(limited to 'parsing/printer.ml')

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 757b61aa1d..dcaac5697b 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -142,11 +142,6 @@ let pr_rawterm t =
   else Ppconstrnew.pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)
 
 open Pattern
-let pr_ref_label = function (* On triche sur le contexte *)
-  | ConstNode sp -> pr_constant (Global.env()) sp
-  | IndNode sp -> pr_inductive (Global.env()) sp
-  | CstrNode sp -> pr_constructor (Global.env()) sp
-  | VarNode id -> pr_id id
 
 let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t
 
-- 
cgit v1.2.3