From 1a43fda0dc9bb8d100808426980446353f8f1ae3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 11:21:23 +0200
Subject: Removing internal support for accepting "{struct x}" and co in
 "Theorem with".

There were actually no syntax for it, and I'm still unsure what good
syntax to give to it, even more that it would be useful to have one.
---
 printing/ppvernac.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'printing/ppvernac.ml')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index cfc2e48d11..d3b4007fbe 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -386,13 +386,12 @@ open Decl_kinds
     ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def
     ++ prlist (pr_decl_notation pr_constr) ntn
 
-  let pr_statement head (idpl,(bl,c,guard)) =
+  let pr_statement head (idpl,(bl,c)) =
     assert (not (Option.is_empty idpl));
     let id, pl = Option.get idpl in
     hov 2
       (head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++
          (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
-         pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
          str":" ++ pr_spc_lconstr c)
 
   let pr_priority = function
-- 
cgit v1.2.3


From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 printing/ppvernac.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'printing/ppvernac.ml')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e4a87739b1..58475630e6 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -395,10 +395,6 @@ open Decl_kinds
          pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
          str":" ++ pr_spc_lconstr c)
 
-  let pr_priority = function
-    | None -> mt ()
-    | Some i -> spc () ++ str "|" ++ spc () ++ int i
-
 (**************************************)
 (* Pretty printer for vernac commands *)
 (**************************************)
-- 
cgit v1.2.3


From c1e9a27d383688e44ba34ada24fe08151cb5846e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 17 May 2017 21:04:18 +0200
Subject: [vernac] Remove `Save thm id.` command.

We'd like to cleanup the `proof_end` type so we can have a smaller
path in proof save. Note that the construction:

```
Goal Type.
⋮
Save id.
```

has to be handled by the STM in the same path as Defined (but with an
opaque flag), as `Save id` will alter the environment and cannot be
processed in parallel.

We thus try to simply such paths a bit, as complexity of `lemmas.ml`
seems like an issue these days. The form `Save Theorem id` doesn't
really seem used, and moreover we should really add a type of "Goal",
and unify syntax.

It is often the case that beginners try `Goal addnC n : n + 0 = n."
etc...
---
 printing/ppvernac.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'printing/ppvernac.ml')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 3e41439c8c..76f1d8dd71 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -721,9 +721,7 @@ open Decl_kinds
               | Opaque (Some l) ->
                   keyword "Qed" ++ spc() ++ str"export" ++
                     prlist_with_sep (fun () -> str", ") pr_lident l)
-          | Some (id,th) -> (match th with
-              | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
-              | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)
+          | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
       )
       | VernacExactProof c ->
         return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
-- 
cgit v1.2.3