aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/g_proofs.ml46
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--parsing/pcoq.ml41
-rw-r--r--parsing/pcoq.mli1
-rw-r--r--toplevel/command.ml18
-rw-r--r--toplevel/command.mli14
-rw-r--r--toplevel/vernacentries.ml58
7 files changed, 37 insertions, 63 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 6903293bb..2ce4211fc 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -50,10 +50,8 @@ GEXTEND Gram
| IDENT "Save" -> <:ast< (SaveNamed) >>
| IDENT "Defined" -> <:ast< (DefinedNamed) >>
| IDENT "Defined"; id = identarg -> <:ast< (DefinedAnonymous $id) >>
- | IDENT "Save"; IDENT "Remark"; id = identarg ->
- <:ast< (SaveAnonymousRmk $id) >>
- | IDENT "Save"; IDENT "Theorem"; id = identarg ->
- <:ast< (SaveAnonymousThm $id) >>
+ | IDENT "Save"; tok = thm_tok; id = identarg ->
+ <:ast< (SaveAnonymous $tok $id) >>
| IDENT "Save"; id = identarg -> <:ast< (SaveAnonymous $id) >>
| IDENT "Suspend" -> <:ast< (SUSPEND) >>
| IDENT "Resume" -> <:ast< (RESUME) >>
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7ed3f645b..76ffec9a4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -51,7 +51,7 @@ END
(* Gallina declarations *)
GEXTEND Gram
- GLOBAL: gallina gallina_ext;
+ GLOBAL: gallina gallina_ext thm_tok;
theorem_body_line:
[ [ n = numarg; ":"; tac = tacarg; "." ->
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 833f8a505..a5af0845b 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -366,6 +366,7 @@ module Vernac_ =
let tacarg = gec "tacarg"
let sortarg = gec "sortarg"
let theorem_body = gec "theorem_body"
+ let thm_tok = gec "thm_tok"
let gallina = gec "gallina"
let gallina_ext = gec "gallina_ext"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7044801fa..20bf35dea 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -178,6 +178,7 @@ module Vernac_ :
val tacarg : Coqast.t Gram.Entry.e
val sortarg : Coqast.t Gram.Entry.e
val theorem_body : Coqast.t Gram.Entry.e
+ val thm_tok : Coqast.t Gram.Entry.e
val gallina : Coqast.t Gram.Entry.e
val gallina_ext : Coqast.t Gram.Entry.e
diff --git a/toplevel/command.ml b/toplevel/command.ml
index c7fcc0f3b..e8bc17cc3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -461,23 +461,19 @@ let save_named opacity =
let id,(const,strength) = Pfedit.cook_proof () in
save opacity id const strength
-let save_anonymous_with_strength opacity save_ident id const strength =
+let check_anonymity id save_ident =
if atompart_of_id id <> "Unnamed_thm" then
- message("Overriding name "^(string_of_id id)^" and using "^save_ident);
- save opacity (id_of_string save_ident) const strength
+ message("Overriding name "^(string_of_id id)^" and using "^save_ident)
let save_anonymous opacity save_ident =
let id,(const,strength) = Pfedit.cook_proof () in
- save_anonymous_with_strength opacity save_ident id const strength
+ check_anonymity id save_ident;
+ save opacity (id_of_string save_ident) const strength
-let save_anonymous_thm opacity save_ident =
+let save_anonymous_with_strength strength opacity save_ident =
let id,(const,_) = Pfedit.cook_proof () in
- save_anonymous_with_strength opacity save_ident id const NeverDischarge
-
-let save_anonymous_remark opacity save_ident =
- let id,(const,_) = Pfedit.cook_proof ()
- and path = try List.tl (List.tl (Lib.cwd())) with Failure _ -> [] in
- save_anonymous_with_strength opacity save_ident id const (make_strength path)
+ check_anonymity id save_ident;
+ save opacity (id_of_string save_ident) const strength
let get_current_context () =
try Pfedit.get_current_goal_context ()
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 83ce53567..b7b9d0f13 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -63,14 +63,14 @@ under the name [name] and respects the strength of the declaration *)
val save_anonymous : bool -> string -> unit
-(* [save_anonymous_thm b name] behaves as [save_named] but declares the
-theorem under the name [name] and gives it the strength of a theorem *)
+(* [save_anonymous_with_strength s b name] behaves as [save_anonymous] but
+ declares the theorem under the name [name] and gives it the
+ strength [strength] *)
-val save_anonymous_thm : bool -> string -> unit
+val save_anonymous_with_strength : strength -> bool -> string -> unit
-(* [save_anonymous_remark b name] behaves as [save_named] but declares the
-theorem under the name [name] and gives it the strength of a remark *)
-
-val save_anonymous_remark : bool -> string -> unit
+(* [get_current_context ()] returns the evar context and env of the
+ current open proof if any, otherwise returns the empty evar context
+ and the current global env *)
val get_current_context : unit -> Proof_type.enamed_declarations * Environ.env
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d56b56602..712e9ff7a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -577,6 +577,17 @@ let _ =
Impargs.declare_implicits (locate_qualid dummy_loc qid))
| _ -> bad_vernac_args "IMPLICITS")
+let interp_definition_kind = function
+ | "THEOREM" -> (NeverDischarge, true)
+ | "LEMMA" -> (NeverDischarge, true)
+ | "FACT" -> (make_strength_1 (), true)
+ | "REMARK" -> (make_strength_0 (), true)
+ | "DEFINITION" -> (NeverDischarge, false)
+ | "LET" -> (make_strength_1 (), false)
+ | "LETTOP" -> (NeverDischarge, false)
+ | "LOCAL" -> (make_strength_0 (), false)
+ | _ -> anomaly "Unexpected definition kind"
+
let _ =
add "SaveNamed"
(function
@@ -603,29 +614,16 @@ let _ =
let _ =
add "SaveAnonymous"
(function
- | [VARG_IDENTIFIER id] ->
- (fun () ->
- if_verbose show_script ();
- save_anonymous true (string_of_id id))
- | _ -> bad_vernac_args "SaveAnonymous")
-
-let _ =
- add "SaveAnonymousThm"
- (function
- | [VARG_IDENTIFIER id] ->
+ | [VARG_STRING kind; VARG_IDENTIFIER id] ->
(fun () ->
+ let (strength, opacity) = interp_definition_kind kind in
if_verbose show_script ();
- save_anonymous_thm true (string_of_id id))
- | _ -> bad_vernac_args "SaveAnonymousThm")
-
-let _ =
- add "SaveAnonymousRmk"
- (function
+ save_anonymous_with_strength strength opacity (string_of_id id))
| [VARG_IDENTIFIER id] ->
(fun () ->
if_verbose show_script ();
- save_anonymous_remark true (string_of_id id))
- | _ -> bad_vernac_args "SaveAnonymousRmk")
+ save_anonymous true (string_of_id id))
+ | _ -> bad_vernac_args "SaveAnonymous")
let _ =
add "TRANSPARENT"
@@ -853,17 +851,7 @@ let _ =
add "StartProof"
(function
| [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR com] ->
- let stre = match kind with
- | "THEOREM" -> NeverDischarge
- | "LEMMA" -> NeverDischarge
- | "FACT" -> make_strength_1 ()
- | "REMARK" -> make_strength_0 ()
- | "DEFINITION" -> NeverDischarge
- | "LET" -> make_strength_2 ()
- | "LETTOP" -> NotDeclare
- | "LOCAL" -> make_strength_0 ()
- | _ -> anomaly "Unexpected string"
- in
+ let stre = fst (interp_definition_kind kind) in
fun () ->
begin
if (kind = "LETTOP") && not(refining ()) then
@@ -885,17 +873,7 @@ let _ =
| _ -> bad_vernac_args "")
coml
in
- let (stre,opacity) = match kind with
- | "THEOREM" -> (NeverDischarge,true)
- | "LEMMA" -> (NeverDischarge,true)
- | "FACT" -> (make_strength_1(),true)
- | "REMARK" -> (make_strength_0(),true)
- | "DEFINITION" -> (NeverDischarge,false)
- | "LET" -> (make_strength_1(),false)
- | "LETTOP" -> (NeverDischarge,false)
- | "LOCAL" -> (make_strength_0(),false)
- | _ -> anomaly "Unexpected string"
- in
+ let (stre,opacity) = interp_definition_kind kind in
(fun () ->
try
States.with_heavy_rollback
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 16:31:59 +0000