diff options
| author | Vincent Laporte | 2019-03-14 17:17:38 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-14 17:17:38 +0000 |
| commit | 710a7cad94dcc9c734ab9ccc425f7a080dddc5f8 (patch) | |
| tree | a98a67f87b7bb2fee9b7f788a71672243825ab05 /plugins | |
| parent | 98914efd4193160d843092461674d6482aeee32e (diff) | |
| parent | 8ea0039ff69491b9e672bc3c522a356085d89c22 (diff) | |
Merge PR #9771: Exposes Coq_micromega.dump_proof_term to allow a use independent from tactics
Reviewed-by: vbgl
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/micromega/coq_micromega.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/plugins/micromega/coq_micromega.mli b/plugins/micromega/coq_micromega.mli index b91feb3984..d1776b8ca4 100644 --- a/plugins/micromega/coq_micromega.mli +++ b/plugins/micromega/coq_micromega.mli @@ -20,3 +20,9 @@ val sos_Q : unit Proofview.tactic -> unit Proofview.tactic val sos_R : unit Proofview.tactic -> unit Proofview.tactic val lra_Q : unit Proofview.tactic -> unit Proofview.tactic val lra_R : unit Proofview.tactic -> unit Proofview.tactic + + +(** {5 Use Micromega independently from tactics. } *) + +(** [dump_proof_term] generates the Coq representation of a Micromega proof witness *) +val dump_proof_term : Micromega.zArithProof -> EConstr.t |