diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
| commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
| tree | 074182834cb406d1304aec4233718564a9c06ba1 /proofs/pfedit.mli | |
| parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) | |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 5e0fb4dd..fc521ea4 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -69,11 +69,11 @@ val start_proof : val cook_this_proof : Proof_global.proof_object -> (Id.t * - (Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) val cook_proof : unit -> (Id.t * - (Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) (** {6 ... } *) (** [get_pftreestate ()] returns the current focused pending proof. @@ -117,7 +117,8 @@ val set_end_tac : Tacexpr.raw_tactic_expr -> unit (** {6 ... } *) (** [set_used_variables l] declares that section variables [l] will be used in the proof *) -val set_used_variables : Id.t list -> Context.section_context +val set_used_variables : + Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list val get_used_variables : unit -> Context.section_context option (** {6 ... } *) @@ -151,9 +152,9 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit val build_constant_by_tactic : Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind -> types -> unit Proofview.tactic -> - Entries.definition_entry * bool * Evd.evar_universe_context + Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context -val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> +val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context |