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

2 files changed, 11 insertions, 10 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 07d8b39bd..1b649194d 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 99b56d484..cbbb54e45 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