diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:24:04 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:24:04 +0100 |
| commit | 374d1efc5de20f8c99c13a7216357a7228c353e8 (patch) | |
| tree | 57c77f168c5b5e0d8164128d7977e2bd0efdfc7f /plugins/extraction/extract_env.mli | |
| parent | a40fb961c8ffeeb03769404cacda8bd6cff17417 (diff) | |
| parent | 940b2f972c4b3f42850e36c721564b127d30e496 (diff) | |
Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish #4129)
Diffstat (limited to 'plugins/extraction/extract_env.mli')
| -rw-r--r-- | plugins/extraction/extract_env.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 464f109be..591d3bb86 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -36,4 +36,9 @@ val print_one_decl : (* Used by Extraction Compute *) val structure_for_compute : - Constr.t -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type + Environ.env -> Evd.evar_map -> EConstr.t -> + Miniml.ml_decl list * Miniml.ml_ast * Miniml.ml_type + +(* Show the extraction of the current ongoing proof *) + +val show_extraction : unit -> unit |