[fleche] [coq] Recognize Goal and Definition $id : ... . as proof…

… starters

Fixes #548 ; it'd be nicer when we switch to the more dynamic method.

Thanks to Théo Zimmerman for reporting the problem.

CHANGES.md

@@ -20,6 +20,8 @@
    early releases, but it doesn't make sense now and made things
    pretty hard to debug on the Windows installer (@ejgallego, #557)
  - Add pointers to Windows installers (@ejgallego, #559)
+ - Recognize `Goal` and `Definition $id : ... .` as proof starters
+   (@ejgallego, #561, reported by @Zimmi48, fixes #548)
 
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------

fleche/doc.ml

@@ -423,7 +423,8 @@ let rec find_proof_start nodes =
   | { Node.ast = None; _ } :: ns -> find_proof_start ns
   | ({ ast = Some ast; _ } as n) :: ns -> (
     match (Node.Ast.to_coq ast).CAst.v.Vernacexpr.expr with
-    | Vernacexpr.VernacSynPure (VernacStartTheoremProof _) ->
+    | Vernacexpr.VernacSynPure (VernacStartTheoremProof _)
+    | VernacSynPure (VernacDefinition (_, _, ProveBody _)) ->
       Some (n, Util.hd_opt ns)
     | _ -> find_proof_start ns)