From af731fbb7f6fb76158c1980eddcc185a7e5e630d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 14 Sep 2001 19:11:06 +0000
Subject: Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold
 nom_local)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1970 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pattern.ml  | 6 +-----
 pretyping/pattern.mli | 1 -
 2 files changed, 1 insertion(+), 6 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index f423777d9b..66125bfeb0 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -50,10 +50,6 @@ type constr_label =
   | IndNode of inductive_path
   | CstrNode of constructor_path
   | VarNode of identifier
-  | SectionVarNode of section_path
-(*
-  | ... 
-*)
 
 exception BoundPattern;;
 
@@ -61,7 +57,7 @@ let label_of_ref = function
   | ConstRef sp     -> ConstNode sp
   | IndRef sp       -> IndNode sp
   | ConstructRef sp -> CstrNode sp
-  | VarRef sp       -> SectionVarNode sp
+  | VarRef sp       -> VarNode (basename sp)
 
 let rec head_pattern_bound t =
   match t with
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index e687e5cbc4..91dd32ba3d 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -38,7 +38,6 @@ type constr_label =
   | IndNode of inductive_path
   | CstrNode of constructor_path
   | VarNode of identifier
-  | SectionVarNode of section_path
 
 val label_of_ref : global_reference -> constr_label
 
-- 
cgit v1.2.3