From 8ea0039ff69491b9e672bc3c522a356085d89c22 Mon Sep 17 00:00:00 2001
From: Chantal Keller
Date: Thu, 14 Mar 2019 08:51:41 +0100
Subject: Exposes Coq_micromega.dump_proof_term to allow a use independent from
 tactics

---
 plugins/micromega/coq_micromega.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'plugins')

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
-- 
cgit v1.2.3