diff options
| author | barras | 2003-12-16 14:05:46 +0000 |
|---|---|---|
| committer | barras | 2003-12-16 14:05:46 +0000 |
| commit | 5eb8860b4326c61e92050a2accebf489d2ebf048 (patch) | |
| tree | 567af1b5e0717002659f877564907beabec8a450 /kernel/environ.ml | |
| parent | a97de9e4814e104dd27b06f4c50718a4cdcdb7f6 (diff) | |
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
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 16 |
1 files changed, 5 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 = |