diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-22 13:10:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-22 13:10:03 +0000 |
| commit | f9031792f714bb468c2dc8bfb49f34cfef44b27a (patch) | |
| tree | 7d67852c2ec622df3520ef08a71a63e9d55b2fd9 /parsing | |
| parent | 2476b8a3397dccc8cadd7422929c844040ecc987 (diff) | |
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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pretty.ml | 2 | ||||
| -rw-r--r-- | parsing/pretty.mli | 5 |
2 files changed, 3 insertions, 4 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 641fa4035..00b598646 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 ae5ce0f25..e10c53b80 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 |