diff options
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 |