diff options
| -rw-r--r-- | kernel/environ.ml | 16 | ||||
| -rw-r--r-- | kernel/sign.ml | 2 | ||||
| -rw-r--r-- | kernel/sign.mli | 3 |
3 files changed, 10 insertions, 11 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 4a2c37a4a..9d81e8f00 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 29e7379e9..40f6e46ad 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 d66421fbd..196d81ca3 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 *) |