From d54b326f1271c4f3dfd207030c153b3e90dcd64b Mon Sep 17 00:00:00 2001
From: Pierre Corbineau
Date: Mon, 2 Mar 2015 14:42:12 +0100
Subject: rewiring Czar printers that were disabled

---
 plugins/decl_mode/ppdecl_proof.mli | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

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

diff --git a/plugins/decl_mode/ppdecl_proof.mli b/plugins/decl_mode/ppdecl_proof.mli
index fd6fb66376..678fc07688 100644
--- a/plugins/decl_mode/ppdecl_proof.mli
+++ b/plugins/decl_mode/ppdecl_proof.mli
@@ -1,2 +1,14 @@
 
-val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds
+open Decl_expr
+open Pptactic
+
+val pr_gen_proof_instr : 
+  ('var -> Pp.std_ppcmds) ->
+  ('constr -> Pp.std_ppcmds) ->
+  ('pat -> Pp.std_ppcmds) ->
+  ('tac -> Pp.std_ppcmds) ->  
+  ('var,'constr,'pat,'tac) gen_proof_instr -> Pp.std_ppcmds
+
+val pr_raw_proof_instr : raw_proof_instr raw_extra_genarg_printer
+val pr_glob_proof_instr : glob_proof_instr glob_extra_genarg_printer
+val pr_proof_instr : proof_instr extra_genarg_printer
-- 
cgit v1.2.3