From a2bdd28d1bdb93664037751b9dc84bcf7d90b6b6 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Sun, 30 Sep 2001 17:54:12 +0000
Subject: Ajout du printer de tactiques + modif du Dynamic ocaml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2086 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/include         | 4 +++-
 dev/top_printers.ml | 2 ++
 2 files changed, 5 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/include b/dev/include
index 2a841e4583..ce923477b2 100644
--- a/dev/include
+++ b/dev/include
@@ -24,4 +24,6 @@
 #install_printer  (* readable_constraints *)  prevc;;
 #install_printer  (* walking_constraints *)  prwc;;
 #install_printer  (* clenv *) prclenv;;
-#install_printer  (* env *) ppenv;;
\ No newline at end of file
+#install_printer  (* env *) ppenv;;
+
+#install_printer  (* tactic *) pptac;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 71347c695a..51334029e5 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -79,6 +79,8 @@ let pp_universes u = pP [< 'sTR"[" ; pr_universes u ; 'sTR"]" >]
 
 let ppenv e = pP (pr_rel_context e (rel_context e))
 
+let pptac = (fun x -> pP(gentacpr x))
+
 let cnt = ref 0
 
 let constr_display csr =
-- 
cgit v1.2.3