diff options
| author | Jason Gross | 2017-06-13 15:42:23 -0400 |
|---|---|---|
| committer | Jason Gross | 2017-06-15 12:20:20 -0400 |
| commit | 8ba5d01a92d5f8fe87c025002fb0bcca8ecef8bc (patch) | |
| tree | 7c523c714d7e558858e64543fab05389a87066e0 | |
| parent | d1d068bcc7ed43d375b1f69a3cc796fb12333519 (diff) | |
API: Hints.run_hint,Pfedit.current_proof_statement
Add them for fiat-parsers
| -rw-r--r-- | API/API.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/API/API.mli b/API/API.mli index 68fbda7c73..8df25bf922 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3947,6 +3947,8 @@ sig val get_current_context : unit -> Evd.evar_map * Environ.env + val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types + (* Deprecated *) val delete_current_proof : unit -> unit [@@ocaml.deprecated "use Proof_global.discard_current"] @@ -4367,6 +4369,8 @@ sig val pp_hints_path : hints_path -> Pp.std_ppcmds val glob_hints_path : Prelude.reference hints_path_gen -> Globnames.global_reference hints_path_gen + val run_hint : hint -> + ((raw_hint * Clenv.clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic val typeclasses_db : hint_db_name val add_hints_init : (unit -> unit) -> unit val create_hint_db : bool -> hint_db_name -> Names.transparent_state -> bool -> unit |