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...
---
 proofs/proof_global.ml  | 2 +-
 proofs/proof_global.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5f4a7766f3..0443d6357f 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -82,7 +82,7 @@ type proof_object = {
 type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
   | Proved of Vernacexpr.opacity_flag *
-             (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+              Vernacexpr.lident option *
               proof_object
 type proof_terminator = proof_ending -> unit
 type closed_proof = proof_object * proof_terminator
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 6bb6f5e2cb..e90fb5bc93 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -70,7 +70,7 @@ type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
 		  proof_universes
   | Proved of Vernacexpr.opacity_flag *
-             (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+              Vernacexpr.lident option *
               proof_object
 type proof_terminator
 type closed_proof = proof_object * proof_terminator
-- 
cgit v1.2.3