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
---
 parsing/printer.ml    | 1 -
 pretyping/pattern.ml  | 6 +-----
 pretyping/pattern.mli | 1 -
 3 files changed, 1 insertion(+), 7 deletions(-)

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 52300882a2..b1a0c65172 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -124,7 +124,6 @@ let pr_ref_label = function (* On triche sur le contexte *)
   | IndNode sp -> pr_inductive (Global.env()) (sp,[||])
   | CstrNode sp -> pr_constructor (Global.env()) (sp,[||])
   | VarNode id -> pr_id id
-  | SectionVarNode sp -> pr_id (basename sp)
 
 let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t)
 let pr_rawterm t = gentermpr (Termast.ast_of_rawconstr t)
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