aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/coq_micromega.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/coq_micromega.mli')
-rw-r--r--plugins/micromega/coq_micromega.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/coq_micromega.mli b/plugins/micromega/coq_micromega.mli
index f2f7fd424f..679290891d 100644
--- a/plugins/micromega/coq_micromega.mli
+++ b/plugins/micromega/coq_micromega.mli
@@ -24,5 +24,5 @@ val print_lia_profile : unit -> unit
(** {5 Use Micromega independently from tactics. } *)
-val dump_proof_term : Micromega.zArithProof -> EConstr.t
(** [dump_proof_term] generates the Coq representation of a Micromega proof witness *)
+val dump_proof_term : Micromega.zArithProof -> EConstr.t