diff options
Diffstat (limited to 'parsing/printmod.ml')
| -rw-r--r-- | parsing/printmod.ml | 31 |
1 files changed, 17 insertions, 14 deletions
diff --git a/parsing/printmod.ml b/parsing/printmod.ml index 16f6e6c9d..9440a61bf 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -97,24 +97,27 @@ and print_modtype locals mty = str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) and print_sig locals sign = - let print_spec (l,spec) = (match spec with - | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition " - | SFBconst {const_body=None} - | SFBconst {const_opaque=true} -> str "Parameter " - | SFBmind _ -> str "Inductive " - | SFBmodule _ -> str "Module " - | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) + let print_spec (l,spec) = str (match spec with + | SFBconst cb -> + (match cb.const_body with + | Def _ -> "Definition " + | Undef _ | OpaqueDef _ -> "Parameter ") + | SFBmind _ -> "Inductive " + | SFBmodule _ -> "Module " + | SFBmodtype _ -> "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_spec sign and print_struct locals struc = - let print_body (l,body) = (match body with - | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition " - | SFBconst {const_body=Some _; const_opaque=true} -> str "Theorem " - | SFBconst {const_body=None} -> str "Parameter " - | SFBmind _ -> str "Inductive " - | SFBmodule _ -> str "Module " - | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) + let print_body (l,body) = str (match body with + | SFBconst cb -> + (match cb.const_body with + | Undef _ -> "Parameter " + | Def _ -> "Definition " + | OpaqueDef _ -> "Theorem ") + | SFBmind _ -> "Inductive " + | SFBmodule _ -> "Module " + | SFBmodtype _ -> "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_body struc |