diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-11 20:14:31 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-11 20:14:31 +0000 |
| commit | 4425c8d353ffdcbed966c253f9624b550626ae0a (patch) | |
| tree | 13e25097ff2865f00dabd37cf3ed6a5748f20e32 /printing | |
| parent | 180a27f8d2b7ba2d7913c37ae01c946acb8c813e (diff) | |
Added a Local Definition vernacular command. This type of definition
has to be refered through its qualified name even when the module
containing it is imported.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16263 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 4a91e1284..850ad2b75 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -327,16 +327,20 @@ let pr_class_rawexpr = function | RefClass qid -> pr_smart_global qid let pr_assumption_token many = function - | (Local,Logical) -> + | (Discharge,Logical) -> str (if many then "Hypotheses" else "Hypothesis") - | (Local,Definitional) -> + | (Discharge,Definitional) -> str (if many then "Variables" else "Variable") | (Global,Logical) -> str (if many then "Axioms" else "Axiom") | (Global,Definitional) -> str (if many then "Parameters" else "Parameter") + | (Local, Logical) -> + str (if many then "Local Axioms" else "Local Axiom") + | (Local,Definitional) -> + str (if many then "Local Parameters" else "Local Parameter") | (Global,Conjectural) -> str"Conjecture" - | (Local,Conjectural) -> + | ((Discharge | Local),Conjectural) -> anomaly (Pp.str "Don't know how to beautify a local conjecture") let pr_params pr_c (xl,(c,t)) = @@ -706,14 +710,14 @@ let rec pr_vernac = function | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_smart_global q | VernacCoercion (s,id,c1,c2) -> hov 1 ( - str"Coercion" ++ (match s with | Local -> spc() ++ - str"Local" ++ spc() | Global -> spc()) ++ + str"Coercion" ++ (if s then spc() ++ + str"Local" ++ spc() else spc()) ++ pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) | VernacIdentityCoercion (s,id,c1,c2) -> hov 1 ( - str"Identity Coercion" ++ (match s with | Local -> spc() ++ - str"Local" ++ spc() | Global -> spc()) ++ pr_lident id ++ + str"Identity Coercion" ++ (if s then spc() ++ + str"Local" ++ spc() else spc()) ++ pr_lident id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) |