diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/lemmas.ml | 32 | ||||
| -rw-r--r-- | vernac/lemmas.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 20 |
3 files changed, 25 insertions, 29 deletions
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 |