From 2253d2eb4f892f932332358be8537fdb5552ef87 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 12 Jun 2017 11:08:12 +0200 Subject: Remove Show Implicit Arguments command. The command has been broken for 15 years. It is basically dead code. Its former behavior can be mimicked with Set Printing Implicit. Show. --- printing/ppvernac.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 781af47892..2633cdd6b5 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -561,7 +561,6 @@ 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" -- cgit v1.2.3 From 6cd14bf253f681d0465f8dce1d84a54a4f104d9c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 12 Jun 2017 11:22:38 +0200 Subject: Remove non-working Show Tree and Show Node commands. --- printing/ppvernac.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 2633cdd6b5..81f41cba13 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -562,11 +562,9 @@ open Decl_kinds let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference 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 -- cgit v1.2.3 From 3813ba5229cf42597cd30a08e842e0832e5253cb Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 12 Jun 2017 11:25:26 +0200 Subject: Remove Show Thesis command which was never implemented. --- printing/ppvernac.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 81f41cba13..9d28bc4f84 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -568,7 +568,6 @@ open Decl_kinds | 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 -> -- cgit v1.2.3 From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 27 Apr 2017 20:16:35 +0200 Subject: Fix bugs and add an option for cumulativity --- printing/ppvernac.ml | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 9d28bc4f84..6a47c308d3 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -727,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":") ++ @@ -754,13 +754,17 @@ 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 + let cm = if cum then "Cumulative" else "NonCumulative" in + cm ^ " " ^ 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) -> -- cgit v1.2.3 From 0c94de1f8c598c1869f71fee86bdbe4f0000a502 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 4 May 2017 19:12:45 +0200 Subject: Add printing of cumulativity in inductive types --- printing/ppvernac.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 6a47c308d3..4a5cfe6301 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -759,8 +759,10 @@ open Decl_kinds | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" | Class _ -> "Class" | Variant -> "Variant" in - let cm = if cum then "Cumulative" else "NonCumulative" in - cm ^ " " ^ kind + 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)) ++ -- cgit v1.2.3 From 94e0cbc26718fe3fecc58f6f8673f5f8abb0ce31 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 21 Jun 2017 15:12:21 +0200 Subject: [vernac] Remove stale bool parameter from `VernacStartTheoremProof` `VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today. --- printing/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 4a5cfe6301..d0536a1744 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -698,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)) -- cgit v1.2.3