From a35f72227565f84c309c057dd9f25229c9a613a5 Mon Sep 17 00:00:00 2001
From: bertot
Date: Fri, 24 Jan 2003 12:53:46 +0000
Subject: Inspect does not work for pcoq and there is no simple fix because
 inspect has not be put among the hooks in the pcoq_hook structure.  As a
 temporary solution, we use a replacement command named "Pcoq_inspect" that
 behaves like Inspect 15.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3610 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/centaur.ml4 | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index f51570394b..a2dcd7e20d 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -956,6 +956,10 @@ VERNAC COMMAND EXTEND StartPcoq
   [ "Start" "Pcoq" "Mode" ] -> [ start_pcoq () ]
 END
 
+VERNAC COMMAND EXTEND Pcoq_inspect
+  [ "Pcoq_inspect" ] -> [ inspect 15 ]
+END
+
 VERNAC COMMAND EXTEND StartPcoqDebug
 | [ "Start" "Pcoq" "Debug" "Mode" ] -> [ start_pcoq_debug () ]
 END
-- 
cgit v1.2.3