diff options
| author | Pierre-Marie Pédrot | 2019-10-03 11:04:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-04 17:57:52 +0200 |
| commit | c0e8d5c0ea52cfb0773ce881e6029f1879b1c7cf (patch) | |
| tree | b50900bb768db5c85e34cf338a09cb3a9d928b20 /tactics | |
| parent | a8ab4cc9bfa9d31ac08b0ae3e3f318578ce50e2a (diff) | |
Remove redundancy in section hypotheses of kernel entries.
We only do it for entries and not declarations because the upper layers
rely on the kernel being able to quickly tell that a definition is improperly
used inside a section. Typically, tactics can mess with the named context
and thus make the use of section definitions illegal. This cannot happen in
the kernel but we cannot remove it due to the code dependency.
Probably fixing a soundness bug reachable via ML code only. We were doing
fancy things w.r.t. computation of the transitive closure of the the variables,
in particular lack of proper sanitization of the kernel input.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 4 | ||||
| -rw-r--r-- | tactics/declare.mli | 2 | ||||
| -rw-r--r-- | tactics/proof_global.ml | 4 | ||||
| -rw-r--r-- | tactics/proof_global.mli | 2 |
4 files changed, 6 insertions, 6 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index e418240d3a..b6a0d9f39a 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -72,7 +72,7 @@ type constant_obj = { type 'a proof_entry = { proof_entry_body : 'a Entries.const_entry_body; (* List of section variables *) - proof_entry_secctx : Constr.named_context option; + proof_entry_secctx : Id.Set.t option; (* State id on which the completion of type checking is reported *) proof_entry_feedback : Stateid.t option; proof_entry_type : Constr.types option; @@ -228,7 +228,7 @@ let cast_opaque_proof_entry e = ids_typ, vars in let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in - keep_hyps env (Id.Set.union hyp_typ hyp_def) + Environ.really_needed env (Id.Set.union hyp_typ hyp_def) | Some hyps -> hyps in { diff --git a/tactics/declare.mli b/tactics/declare.mli index 4cb876cecb..da66a2713c 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -23,7 +23,7 @@ open Entries type 'a proof_entry = { proof_entry_body : 'a Entries.const_entry_body; (* List of section variables *) - proof_entry_secctx : Constr.named_context option; + proof_entry_secctx : Id.Set.t option; (* State id on which the completion of type checking is reported *) proof_entry_feedback : Stateid.t option; proof_entry_type : Constr.types option; diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index a2929e45cd..b723922642 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -36,7 +36,7 @@ type opacity_flag = Opaque | Transparent type t = { endline_tactic : Genarg.glob_generic_argument option - ; section_vars : Constr.named_context option + ; section_vars : Id.Set.t option ; proof : Proof.t ; udecl: UState.universe_decl (** Initial universe declarations *) @@ -128,7 +128,7 @@ let set_used_variables ps l = if not (Option.is_empty ps.section_vars) then CErrors.user_err Pp.(str "Used section variables can be declared only once"); (* EJGA: This is always empty thus we should modify the type *) - (ctx, []), { ps with section_vars = Some ctx} + (ctx, []), { ps with section_vars = Some (Context.Named.to_vars ctx) } let get_open_goals ps = let Proof.{ goals; stack; shelf } = Proof.data ps.proof in diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index d15e23c2cc..b9d1b37a11 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -17,7 +17,7 @@ type t (* Should be moved into a proper view *) val get_proof : t -> Proof.t val get_proof_name : t -> Names.Id.t -val get_used_variables : t -> Constr.named_context option +val get_used_variables : t -> Names.Id.Set.t option (** Get the universe declaration associated to the current proof. *) val get_universe_decl : t -> UState.universe_decl |