From 64feb1a81d7cfb34b72760be3b0fe852ae8aa16f Mon Sep 17 00:00:00 2001
From: bertot
Date: Tue, 3 Apr 2001 11:13:49 +0000
Subject: Export a function (build_inductive) that is used in the graphical
 interface.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1524 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pretty.mli | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index c3bf165b1a..b84c566348 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -34,6 +34,9 @@ val print_judgment : env -> unsafe_judgment -> std_ppcmds
 val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds
 val print_eval :
   'a reduction_function -> env -> unsafe_judgment -> std_ppcmds
+(* This function is exported for the graphical user-interface pcoq *)
+val build_inductive : section_path -> int ->
+  global_reference * rel_context * types * identifier array * types array
 val print_mutual : section_path -> std_ppcmds
 val print_name : Nametab.qualid -> std_ppcmds
 val print_opaque_name : Nametab.qualid -> std_ppcmds
-- 
cgit v1.2.3