From e42f575b22ff2d2a69951227e8c2dd67fd0ab3ee Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 22 Jan 2018 08:26:17 +0000 Subject: [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition --- stm/stm.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm/stm.ml') diff --git a/stm/stm.ml b/stm/stm.ml index 5f4fe6565..ba6c90011 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -547,7 +547,7 @@ end = struct (* {{{ *) let reachable id = reachable !vcs id let mk_branch_name { expr = x } = Branch.make (match Vernacprop.under_control x with - | VernacDefinition (_,((_,i),_),_) -> Id.to_string i + | VernacDefinition (_,((_, Name i),_),_) -> Id.to_string i | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Id.to_string i | _ -> "branch") let edit_branch = Branch.make "edit" -- cgit v1.2.3 From 5b8b60508d74bfe5e436ce182889ad8ee6ca3983 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 25 Jan 2018 16:52:00 +0000 Subject: [vernac] Mutual theorems (VernacStartTheoremProof) always have names --- intf/vernacexpr.ml | 2 +- parsing/g_vernac.ml4 | 4 ++-- printing/ppvernac.ml | 2 -- stm/stm.ml | 2 +- stm/vernac_classifier.ml | 3 +-- vernac/lemmas.ml | 32 ++++++++++++++------------------ vernac/lemmas.mli | 2 ++ vernac/vernacentries.ml | 20 +++++++++----------- 8 files changed, 30 insertions(+), 37 deletions(-) (limited to 'stm/stm.ml') diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index d954ae903..8e0fe54c5 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -210,7 +210,7 @@ type typeclass_constraint = name_decl * binding_kind * constr_expr and typeclass_context = typeclass_constraint list type proof_expr = - ident_decl option * (local_binder_expr list * constr_expr) + ident_decl * (local_binder_expr list * constr_expr) type syntax_modifier = | SetItemLevel of string list * Extend.production_level diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 316b26f20..3244b0ff2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -149,8 +149,8 @@ GEXTEND Gram [ [ thm = thm_token; id = ident_decl; bl = binders; ":"; c = lconstr; l = LIST0 [ "with"; id = ident_decl; bl = binders; ":"; c = lconstr -> - (Some id,(bl,c)) ] -> - VernacStartTheoremProof (thm, (Some id,(bl,c))::l) + (id,(bl,c)) ] -> + VernacStartTheoremProof (thm, (id,(bl,c))::l) | stre = assumption_token; nl = inline; bl = assum_list -> VernacAssumption (stre, nl, bl) | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list -> diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index cea2ec35a..950246c53 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -391,8 +391,6 @@ open Decl_kinds ++ prlist (pr_decl_notation pr_constr) ntn let pr_statement head (idpl,(bl,c)) = - assert (not (Option.is_empty idpl)); - let idpl = Option.get idpl in hov 2 (head ++ spc() ++ pr_ident_decl idpl ++ spc() ++ (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ diff --git a/stm/stm.ml b/stm/stm.ml index ba6c90011..ef599fd48 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -548,7 +548,7 @@ end = struct (* {{{ *) let mk_branch_name { expr = x } = Branch.make (match Vernacprop.under_control x with | VernacDefinition (_,((_, Name i),_),_) -> Id.to_string i - | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Id.to_string i + | VernacStartTheoremProof (_,[((_,i),_),_]) -> Id.to_string i | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2a6a47b02..cbbb54e45 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -93,8 +93,7 @@ let classify_vernac e = let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in VtStartProof(default_proof_mode (),guarantee, idents_of_name i), VtLater | VernacStartTheoremProof (_,l) -> - let ids = - CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in + let ids = List.map (fun (((_, i), _), _) -> i) l in let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in VtStartProof (default_proof_mode (),guarantee,ids), VtLater | VernacFixpoint (discharge,l) -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 6ef310837..57436784b 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -210,17 +210,16 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook = let default_thm_id = Id.of_string "Unnamed_thm" -let compute_proof_name locality = function - | Some ((loc,id),pl) -> - (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || - locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) - then - user_err ?loc (Id.print id ++ str " already exists."); - id - | None -> - let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in - next_global_ident_away default_thm_id avoid +let fresh_name_for_anonymous_theorem () = + let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in + next_global_ident_away default_thm_id avoid + +let check_name_freshness locality (loc,id) : unit = + (* We check existence here: it's a bit late at Qed time *) + if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || + locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) + then + user_err ?loc (Id.print id ++ str " already exists.") let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) = let t_i = norm t_i in @@ -435,20 +434,17 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook = let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in let decl = fst (List.hd thms) in - let evd, decl = - match decl with - | None -> Evd.from_env env0, Univdecls.default_univ_decl - | Some decl -> - Univdecls.interp_univ_decl_opt env0 (snd decl) in - let evd, thms = List.fold_left_map (fun evd (sopt,(bl,t)) -> + let evd, decl = Univdecls.interp_univ_decl_opt env0 (snd decl) in + let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) -> let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in let flags = all_and_fail_flags in let flags = { flags with use_hook = inference_hook } in let evd = solve_remaining_evars flags env evd Evd.empty in let ids = List.map RelDecl.get_name ctx in + check_name_freshness (pi1 kind) id; (* XXX: The nf_evar is critical !! *) - evd, (compute_proof_name (pi1 kind) sopt, + evd, (snd id, (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps')))) evd thms in diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index ca92e856b..126dcd8b0 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -52,6 +52,8 @@ val standard_proof_terminator : Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator +val fresh_name_for_anonymous_theorem : unit -> Id.t + (** {6 ... } *) (** A hook the next three functions pass to cook_proof *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index a0109b231..15a807e58 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -483,30 +483,28 @@ let vernac_definition ~atts discharge kind ((loc, id), pl) def = | Local | Global -> Dumpglob.dump_definition lid false "def" in let program_mode = Flags.is_program_mode () in + let name = + match id with + | Anonymous -> fresh_name_for_anonymous_theorem () + | Name n -> n + in (match def with | ProveBody (bl,t) -> (* local binders, typ *) - start_proof_and_print (local, atts.polymorphic, DefinitionBody kind) - [(match id with - | Anonymous -> None - | Name n -> Some ((loc, n), pl) - ), (bl, t)] hook + start_proof_and_print (local, atts.polymorphic, DefinitionBody kind) + [((loc, name), pl), (bl, t)] hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None | Some r -> let sigma, env = Pfedit.get_current_context () in Some (snd (Hook.get f_interp_redexp env sigma r)) in - ComDefinition.do_definition ~program_mode - (match id with Name n -> n | Anonymous -> assert false) + ComDefinition.do_definition ~program_mode name (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook) let vernac_start_proof ~atts kind l = let local = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then - List.iter (fun (id, _) -> - match id with - | Some (lid,_) -> Dumpglob.dump_definition lid false "prf" - | None -> ()) l; + List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; start_proof_and_print (local, atts.polymorphic, Proof kind) l no_hook let vernac_end_proof ?proof = function -- cgit v1.2.3