[vernac] Mutual theorems (VernacStartTheoremProof) always have names

8 files changed, 30 insertions, 37 deletions

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