diff options
| author | bertot | 2001-04-03 11:13:49 +0000 |
|---|---|---|
| committer | bertot | 2001-04-03 11:13:49 +0000 |
| commit | 64feb1a81d7cfb34b72760be3b0fe852ae8aa16f (patch) | |
| tree | 9fe930eb27288bdc2c531126bde2ec5e34228804 | |
| parent | 9fe35b8a391d301054e41470938b223a90abeb6e (diff) | |
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
| -rw-r--r-- | parsing/pretty.mli | 3 |
1 files changed, 3 insertions, 0 deletions
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 |