From 161e0e8073e84ab0f3e982baf7f7122dd3ddfb85 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 24 Jan 2001 22:26:14 +0000
Subject: Prise en compte des noms longs dans les Hints et les Coercions, et
 réorganisations diverses

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1271 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pattern.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 5c5c28ba1b..d69b5e7242 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -30,6 +30,8 @@ type constr_label =
   | VarNode of identifier
   | SectionVarNode of section_path
 
+val label_of_ref : global_reference -> constr_label
+
 exception BoundPattern
 
 (* [head_pattern_bound t] extracts the head variable/constant of the
-- 
cgit v1.2.3