Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition

10 files changed, 74 insertions, 59 deletions

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 8bd2da2f11..8e0fe54c55 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -167,6 +167,7 @@ type option_ref_value =
 type universe_decl_expr = (Id.t Loc.located list, glob_constraint list) gen_universe_decl
 
 type ident_decl = lident * universe_decl_expr option
+type name_decl = lname * universe_decl_expr option
 
 type sort_expr = Sorts.family
 
@@ -204,12 +205,12 @@ type inductive_expr =
 type one_inductive_expr =
   ident_decl * local_binder_expr list * constr_expr option * constructor_expr list
 
-type typeclass_constraint = (Name.t Loc.located * universe_decl_expr option) * binding_kind * constr_expr
+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
@@ -339,7 +340,7 @@ type nonrec vernac_expr =
   | VernacNotationAddFormat of string * string * string
 
   (* Gallina *)
-  | VernacDefinition of (discharge * definition_object_kind) * ident_decl * definition_expr
+  | VernacDefinition of (discharge * definition_object_kind) * name_decl * definition_expr
   | VernacStartTheoremProof of theorem_kind * proof_expr list
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
@@ -449,7 +450,6 @@ type nonrec vernac_expr =
   | VernacComments of comment list
 
   (* Proof management *)
-  | VernacGoal of constr_expr
   | VernacAbort of lident option
   | VernacAbortAll
   | VernacRestart
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index d88f6fa0dc..1c3ba78376 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -28,7 +28,8 @@ GEXTEND Gram
     | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ]
   ;
   command:
-    [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
+    [ [ IDENT "Goal"; c = lconstr ->
+        VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((Loc.tag ~loc:!@loc Names.Anonymous), None), ProveBody ([], c))
       | IDENT "Proof" -> VernacProof (None,None)
       | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
       | IDENT "Proof"; c = lconstr -> VernacExactProof c
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d498bda341..3244b0ff2b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -133,6 +133,12 @@ let test_plural_form_types loc kwd = function
      warn_plural_command ~loc:!@loc kwd
   | _ -> ()
 
+let lname_of_lident : lident -> lname =
+  Loc.map (fun s -> Name s)
+
+let name_of_ident_decl : ident_decl -> name_decl =
+  on_fst lname_of_lident
+
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
@@ -143,17 +149,17 @@ 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 ->
 	  test_plural_form loc kwd bl;
 	  VernacAssumption (stre, nl, bl)
       | d = def_token; id = ident_decl; b = def_body ->
-          VernacDefinition (d, id, b)
+          VernacDefinition (d, name_of_ident_decl id, b)
       | IDENT "Let"; id = identref; b = def_body ->
-          VernacDefinition ((DoDischarge, Let), (id, None), b)
+          VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b)
       (* Gallina inductive declarations *)
       | cum = cumulativity_token; priv = private_token; f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
@@ -623,12 +629,12 @@ GEXTEND Gram
 	  VernacCanonical (ByNotation ntn)
       | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
           let s = coerce_reference_to_id qid in
-          VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag s),None),d)
+          VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag (Name s)),None),d)
 
       (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = coerce_reference_to_id qid in
-          VernacDefinition ((NoDischarge,Coercion),((Loc.tag s),None),d)
+          VernacDefinition ((NoDischarge,Coercion),((Loc.tag (Name s)),None),d)
       | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
          s = class_rawexpr; ">->"; t = class_rawexpr ->
            VernacIdentityCoercion (f, s, t)
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index c0479dd24b..d74ad06b34 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -553,7 +553,7 @@ GEXTEND Gram
           let s = coerce_reference_to_id qid in
     Vernacexpr.VernacDefinition
       ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure),
-          ((Loc.tag s),None), d)
+          ((Loc.tag (Name s)),None), d)
   ]];
 END
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 7e68a97e44..950246c531 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -71,6 +71,9 @@ open Decl_kinds
     | Some loc -> let (b,_) = Loc.unloc loc in
                   pr_located pr_fqid @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (string_of_fqid fqid))) fqid
 
+  let pr_lname_decl (n, u) =
+    pr_lname n ++ pr_universe_decl u
+
   let pr_smart_global = Pputils.pr_or_by_notation pr_reference
 
   let pr_ltac_ref = Libnames.pr_reference
@@ -388,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()) ++
@@ -562,8 +563,6 @@ open Decl_kinds
         return (keyword "Unfocus")
       | VernacUnfocused ->
         return (keyword "Unfocused")
-      | VernacGoal c ->
-        return (keyword "Goal" ++ pr_lconstrarg c)
       | VernacAbort id ->
         return (keyword "Abort" ++ pr_opt pr_lident id)
       | VernacUndo i ->
@@ -674,7 +673,10 @@ open Decl_kinds
       (* Gallina *)
       | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *)
         let pr_def_token dk =
-          keyword (Kindops.string_of_definition_object_kind dk)
+          keyword (
+            if Name.is_anonymous (snd (fst id))
+            then "Goal"
+            else Kindops.string_of_definition_object_kind dk)
         in
         let pr_reduce = function
           | None -> mt()
@@ -691,12 +693,13 @@ open Decl_kinds
             in
             (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
           | ProveBody (bl,t) ->
-            (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in
+            let typ u = if snd (fst id) = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in
+            (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in
         let (binds,typ,c) = pr_def_body b in
         return (
           hov 2 (
             pr_def_token kind ++ spc()
-            ++ pr_ident_decl id ++ binds ++ typ
+            ++ pr_lname_decl id ++ binds ++ typ
             ++ (match c with
               | None -> mt()
               | Some cc -> str" :=" ++ spc() ++ cc))
diff --git a/stm/stm.ml b/stm/stm.ml
index 07d8b39bd2..1b649194d5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -566,8 +566,8 @@ 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
-    | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Id.to_string i
+    | VernacDefinition (_,((_, Name 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 99b56d4846..cbbb54e45b 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -48,6 +48,11 @@ let declare_vernac_classifier
 =
   classifiers := !classifiers @ [s,f]
 
+let idents_of_name : Names.Name.t -> Names.Id.t list =
+  function
+  | Names.Anonymous -> []
+  | Names.Name n -> [n]
+
 let classify_vernac e =
   let static_classifier ~poly e = match e with
     (* Univ poly compatibility: we run it now, so that we can just
@@ -83,18 +88,14 @@ let classify_vernac e =
     | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
     (* StartProof *)
     | VernacDefinition ((Decl_kinds.DoDischarge,_),((_,i),_),ProveBody _) ->
-        VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
+        VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
     | VernacDefinition (_,((_,i),_),ProveBody _) ->
        let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-        VtStartProof(default_proof_mode (),guarantee,[i]), VtLater
+        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
-    | VernacGoal _ ->
-       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-       VtStartProof (default_proof_mode (),guarantee,[]), VtLater
     | VernacFixpoint (discharge,l) ->
        let guarantee =
          if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
@@ -121,7 +122,7 @@ let classify_vernac e =
     | VernacAssumption (_,_,l) ->
         let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in
         VtSideff ids, VtLater    
-    | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater
+    | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff (idents_of_name id), VtLater
     | VernacInductive (_, _,_,l) ->
         let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with
         | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 6ef310837c..57436784b8 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 ca92e856bc..126dcd8b07 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 1a02a22a5c..15a807e585 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -471,33 +471,40 @@ let vernac_definition_hook p = function
 | SubClass -> Class.add_subclass_hook p
 | _ -> no_hook
 
-let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def =
+let vernac_definition ~atts discharge kind ((loc, id), pl) def =
   let local = enforce_locality_exp atts.locality discharge in
   let hook = vernac_definition_hook atts.polymorphic kind in
-  let () = match local with
-  | Discharge -> Dumpglob.dump_definition lid true "var"
-  | Local | Global -> Dumpglob.dump_definition lid false "def"
+  let () =
+    match id with
+    | Anonymous -> ()
+    | Name n -> let lid = (loc, n) in
+      match local with
+      | Discharge -> Dumpglob.dump_definition lid true "var"
+      | 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)
-	    [Some (lid,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 id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook)
+      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
@@ -2068,7 +2075,6 @@ let interp ?proof ~atts ~st c =
   | VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n")
 
   (* Proof management *)
-  | VernacGoal t -> vernac_start_proof ~atts Theorem [None,([],t)]
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
   | VernacUnfocused -> vernac_unfocused ()