From f9031792f714bb468c2dc8bfb49f34cfef44b27a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 22 May 2000 13:10:03 +0000
Subject: Suite restructuration inductifs; changement nom module Constant en
 Declarations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@458 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pretty.ml  | 2 +-
 parsing/pretty.mli | 5 ++---
 2 files changed, 3 insertions(+), 4 deletions(-)

(limited to 'parsing')

diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 641fa40356..00b598646c 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -6,7 +6,7 @@ open Util
 open Names
 open Generic
 open Term
-open Constant
+open Declarations
 open Inductive
 open Sign
 open Reduction
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index ae5ce0f252..e10c53b802 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -31,9 +31,8 @@ val print_val : env -> unsafe_judgment -> std_ppcmds
 val print_type : env -> unsafe_judgment -> std_ppcmds
 val print_eval :
   'a reduction_function -> env -> unsafe_judgment -> std_ppcmds
-val implicit_args_msg : 
-  section_path -> Constant.mutual_inductive_packet array -> std_ppcmds
-val print_mutual : section_path -> Constant.mutual_inductive_body -> std_ppcmds
+val print_mutual :
+  section_path -> Declarations.mutual_inductive_body -> std_ppcmds
 val print_name : identifier -> std_ppcmds
 val print_opaque_name : identifier -> std_ppcmds
 val print_local_context : unit -> std_ppcmds
-- 
cgit v1.2.3