From a615382472ee21e288bd7115be147415e465e897 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 16 Mar 2015 17:56:48 +0100
Subject: Declarative mode: plug the specialised printers back.

It will not work in CoqIDE though, which handles printing its own way. It's a general remark that we have many ways of printing things in Coq and we should look for a unified structured framework to be shared between interfaces.
---
 plugins/decl_mode/decl_mode.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'plugins/decl_mode/decl_mode.mli')

diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index e12c4c9237..fd7e15c150 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -72,6 +72,8 @@ val get_last:  Environ.env -> Id.t
 (** [get_last] raises a [UserError] when it cannot find a previous
     statement in the environment. *)
 
+val get_end_command : Proof.proof -> string
+
 val focus : Proof.proof -> unit
 
 val unfocus : unit -> unit
-- 
cgit v1.2.3