diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | dev/v8-syntax/syntax-v8.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 8 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 4 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 6 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 4 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 2 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 11 |
9 files changed, 12 insertions, 29 deletions
@@ -28,6 +28,8 @@ Vernacular Commands - Goals context can be printed in a more compact way when "Set Printing Compact Contexts" is activated. +- The deprecated `Save` vernacular and its form `Save Theorem id` to + close proofs have been removed from the syntax. Please use `Qed`. Standard Library diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 64431ea16..fa2864cec 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -1158,7 +1158,7 @@ $$ \nlsep \TERM{Abort}~\NT{ident} \nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body} \nlsep \TERM{Qed} -\nlsep \TERM{Save}~\OPTGR{\NT{thm-token}~\NT{ident}} +\nlsep \TERM{Save}~\NT{ident}} \nlsep \TERM{Defined}~\OPT{\NT{ident}} \nlsep \TERM{Suspend} \nlsep \TERM{Resume}~\OPT{\NT{ident}} diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 7e2b9db24..0760d716e 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -96,14 +96,6 @@ memory overflow. (and the following ones) can only be used if the original goal has been opened using the {\tt Goal} command. -\item {\tt Save Theorem {\ident}.} \\ - {\tt Save Lemma {\ident}.} \\ - {\tt Save Remark {\ident}.}\\ - {\tt Save Fact {\ident}.} - {\tt Save Corollary {\ident}.} - {\tt Save Proposition {\ident}.} - - Are equivalent to {\tt Save {\ident}.} \end{Variants} \subsection[\tt Admitted.]{\tt Admitted.\comindex{Admitted}\label{Admitted}} diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index cb093d85d..94fa37eb6 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -143,6 +143,7 @@ type search_restriction = type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) + (* list of idents for qed exporting *) type opacity_flag = Opaque of lident list option | Transparent type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option @@ -223,7 +224,8 @@ type syntax_modifier = type proof_end = | Admitted - | Proved of opacity_flag * (lident * theorem_kind option) option + (* name in `Save ident` when closing goal *) + | Proved of opacity_flag * lident option type scheme = | InductionScheme of bool * reference or_by_notation * sort_expr diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 53637439a..2def22290 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -48,13 +48,11 @@ GEXTEND Gram | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None)) | IDENT "Qed"; IDENT "exporting"; l = LIST0 identref SEP "," -> VernacEndProof (Proved (Opaque (Some l),None)) - | IDENT "Save"; tok = thm_token; id = identref -> - VernacEndProof (Proved (Opaque None,Some (id,Some tok))) | IDENT "Save"; id = identref -> - VernacEndProof (Proved (Opaque None,Some (id,None))) + VernacEndProof (Proved (Opaque None, Some id)) | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None)) | IDENT "Defined"; id=identref -> - VernacEndProof (Proved (Transparent,Some (id,None))) + VernacEndProof (Proved (Transparent,Some id)) | IDENT "Restart" -> VernacRestart | IDENT "Undo" -> VernacUndo 1 | IDENT "Undo"; n = natural -> VernacUndo n diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 3e41439c8..76f1d8dd7 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)) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 5f4a7766f..0443d6357 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 6bb6f5e2c..e90fb5bc9 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 diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index b79795aeb..0088b7079 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -280,13 +280,6 @@ let save_anonymous ?export_seff proof save_ident = check_anonymity id save_ident; save ?export_seff save_ident const cstrs pl do_guard persistence hook -let save_anonymous_with_strength ?export_seff proof kind save_ident = - let id,const,(cstrs,pl),do_guard,_,hook = proof in - check_anonymity id save_ident; - (* we consider that non opaque behaves as local for discharge *) - save ?export_seff save_ident const cstrs pl do_guard - (Global, const.const_entry_polymorphic, Proof kind) hook - (* Admitted *) let warn_let_as_axiom = @@ -337,9 +330,7 @@ let universe_proof_terminator compute_guard hook = (hook (Some (fst proof.Proof_global.universes))) is_opaque in begin match idopt with | None -> save_named ~export_seff proof - | Some ((_,id),None) -> save_anonymous ~export_seff proof id - | Some ((_,id),Some kind) -> - save_anonymous_with_strength ~export_seff proof kind id + | Some (_,id) -> save_anonymous ~export_seff proof id end; check_exist exports end |