[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition

8 files changed, 50 insertions, 28 deletions

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 8bd2da2f1..d954ae903 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,7 +205,7 @@ 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
 
@@ -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 d88f6fa0d..1c3ba7837 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 d498bda34..316b26f20 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
@@ -151,9 +157,9 @@ GEXTEND Gram
 	  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 c0479dd24..d74ad06b3 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 7e68a97e4..cea2ec35a 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
@@ -562,8 +565,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 +675,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 +695,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 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"
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 99b56d484..2a6a47b02 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,15 @@ 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 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 +123,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/vernacentries.ml b/vernac/vernacentries.ml
index 1a02a22a5..a0109b231 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -471,25 +471,34 @@ 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
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
           start_proof_and_print (local, atts.polymorphic, DefinitionBody kind)
-	    [Some (lid,pl), (bl,t)] hook
+            [(match id with
+                | Anonymous -> None
+                | Name n -> Some ((loc, n), 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
+        (match id with Name n -> n | Anonymous -> assert false)
+        (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
@@ -2068,7 +2077,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 ()