diff options
| author | William Lawvere | 2017-07-01 22:10:46 -0700 |
|---|---|---|
| committer | William Lawvere | 2017-07-01 22:10:46 -0700 |
| commit | 80649ebaba75838bfd28ae78822cd2c078da4b23 (patch) | |
| tree | ac29ab5edd3921dbee1c2256737347fd1542dc67 /printing/ppvernac.ml | |
| parent | c2942e642ee6f83cc997f9a2510cdb7446a65cb4 (diff) | |
| parent | 35e0f327405fb659c7ec5f9f7d26ea284aa45810 (diff) | |
Merge remote-tracking branch 'upstream/trunk' into trunk
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 781af47892..d0536a1744 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -561,17 +561,13 @@ open Decl_kinds | GoalUid n -> spc () ++ str n in let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n - | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n | ShowProof -> keyword "Show Proof" - | ShowNode -> keyword "Show Node" | ShowScript -> keyword "Show Script" | ShowExistentials -> keyword "Show Existentials" | ShowUniverses -> keyword "Show Universes" - | ShowTree -> keyword "Show Tree" | ShowProofNames -> keyword "Show Conjectures" | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") | ShowMatch id -> keyword "Show Match " ++ pr_reference id - | ShowThesis -> keyword "Show Thesis" in return (pr_showable s) | VernacCheckGuard -> @@ -702,7 +698,7 @@ open Decl_kinds | Some cc -> str" :=" ++ spc() ++ cc)) ) - | VernacStartTheoremProof (ki,l,_) -> + | VernacStartTheoremProof (ki,l) -> return ( hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++ prlist (pr_statement (spc () ++ keyword "with")) (List.tl l)) @@ -731,7 +727,7 @@ open Decl_kinds let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in return (hov 2 (pr_assumption_token (n > 1) stre ++ pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions)) - | VernacInductive (p,f,l) -> + | VernacInductive (cum, p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ @@ -758,13 +754,19 @@ open Decl_kinds in let key = let (_,_,_,k,_),_ = List.hd l in - match k with Record -> "Record" | Structure -> "Structure" - | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" - | Class _ -> "Class" | Variant -> "Variant" + let kind = + match k with Record -> "Record" | Structure -> "Structure" + | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" + | Class _ -> "Class" | Variant -> "Variant" + in + if p then + let cm = if cum then "Cumulative" else "NonCumulative" in + cm ^ " " ^ kind + else kind in return ( hov 1 (pr_oneind key (List.hd l)) ++ - (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) + (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) | VernacFixpoint (local, recs) -> |