diff options
| author | Chantal Keller | 2019-03-14 08:51:41 +0100 |
|---|---|---|
| committer | Chantal Keller | 2019-03-14 08:51:41 +0100 |
| commit | 8ea0039ff69491b9e672bc3c522a356085d89c22 (patch) | |
| tree | aff20d37f8b6ef3607226a996289ad21de0272c2 /plugins | |
| parent | 27ab0d69e87fa3ce414cdaa205f7f6266693e263 (diff) | |
Exposes Coq_micromega.dump_proof_term to allow a use independent from tactics
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 |