bug #266 (Search Error si on calcule apres avoir fait Clear d'une var Local)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5101 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 10 insertions, 11 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4a2c37a4ab..9d81e8f001 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -200,11 +200,11 @@ let set_engagement c env = (* Unsafe *)
 (* Lookup of section variables *)
 let lookup_constant_variables c env =
   let cmap = lookup_constant c env in
-  Sign.instance_from_named_context cmap.const_hyps
+  Sign.vars_of_named_context cmap.const_hyps
 
 let lookup_inductive_variables (kn,i) env =
   let mis = lookup_mind kn env in
-  Sign.instance_from_named_context mis.mind_hyps
+  Sign.vars_of_named_context mis.mind_hyps
 
 let lookup_constructor_variables (ind,_) env =
   lookup_inductive_variables ind env
@@ -214,15 +214,9 @@ let lookup_constructor_variables (ind,_) env =
 let vars_of_global env constr =
   match kind_of_term constr with
       Var id -> [id]
-    | Const kn ->
-        List.map destVar 
-          (Array.to_list (lookup_constant_variables kn env))
-    | Ind ind ->
-        List.map destVar 
-          (Array.to_list (lookup_inductive_variables ind env))
-    | Construct cstr ->
-        List.map destVar 
-          (Array.to_list (lookup_constructor_variables cstr env))
+    | Const kn -> lookup_constant_variables kn env
+    | Ind ind -> lookup_inductive_variables ind env
+    | Construct cstr -> lookup_constructor_variables cstr env
     | _ -> []
 
 let global_vars_set env constr = 
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 29e7379e92..40f6e46ad1 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -28,6 +28,8 @@ let rec lookup_named id = function
 
 let named_context_length = List.length
 
+let vars_of_named_context = List.map (fun (id,_,_) -> id)
+
 let instance_from_named_context sign =
   let rec inst_rec = function
     | (id,None,_) :: sign -> mkVar id :: inst_rec sign
diff --git a/kernel/sign.mli b/kernel/sign.mli
index d66421fbd1..196d81ca3b 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -20,8 +20,11 @@ type section_context = named_context
 
 val empty_named_context : named_context
 val add_named_decl : named_declaration -> named_context -> named_context
+val vars_of_named_context : named_context -> identifier list
 
 val lookup_named : identifier -> named_context -> named_declaration
+
+(* number of declarations *)
 val named_context_length : named_context -> int
 
 (*s Recurrence on [named_context]: older declarations processed first *)