diff options
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 |