Coq Error Syntax error: '.' expected after [gallina] (in [vernac_aux])

So I have this code:

Require Import Unicode.Utf8.
Require Import String.

Inductive AExp :=
| avar : string → AExp 
| anum : nat → AExp 
| aplus : AExp → AExp → AExp 
| amul : AExp → AExp → AExp.

Coercion anum : nat >-> AExp.
Coercion avar : string >-> AExp.
Notation "A +' B" := (aplus A B) (at level 50, left associativity).
Notation "A *' B" := (amul A B) (at level 40, left associativity).

Inductive BExp :=
| btrue : BExp
| bfalse : BExp
| bnot : BExp → BExp
| band : BExp → BExp → BExp
| blessthan : AExp → AExp → BExp
| bgreaterthan : AExp → AExp → BExp.

Notation "A <' B" := (blessthan A B) (at level 80).
Notation "A >' B" := (bgreaterthan A B) (at level 80).
Infix "and'" := band (at level 82).
Notation "! A" := (bnot A) (at level 81).

Inductive Stmt :=
| assignment : string → AExp → Stmt 
| while : BExp → list Stmt → Stmt
| seq : Stmt → Stmt → Stmt
| obj_inst : string → string → Stmt
| method_invoke : string → string → list AExp → Stmt.

Notation "X ::= A" := (assignment X A) (at level 85).
Notation "S1 ;; S2" := (seq S1 S2) (at level 99, right associativity).

Inductive Method :=
| method : string → list Stmt → Method.

Inductive Class :=
| class : string → list (string * AExp) → list Method → Class.

Definition Point :=
  class "Point"
    [("x", anum 0) ("y", anum 0)]
    [
      method "move" [
        assignment "x" (aplus (avar "x") (anum 1));
        assignment "y" (aplus (avar "y") (anum 1))
      ]
    ].

Definition CreatePoint : Stmt :=
  obj_inst "p" "Point".

Definition MovePoint : Stmt :=
  method_invoke "p" "move" [].

Definition SampleProgram :=
  seq CreatePoint MovePoint.

and I got this error:

Syntax error: '.' expected after [gallina] (in [vernac_aux]). And I am not sure if it's because of the Definition Point.

Tried using chatGpt and it didn't work. Using it I wasted a lot of time. (i don't know what to write mroe so StackOverflow would let me post this question)

(Looks like some old Coq code that needs some freshening up.)

Typically, you cannot use notations without importing/opening them: and your code is missing both list and string notations.

Here is the fix for that, as well as a fix to the StdLib imports, as with your code you could have name conflicts/ambiguities:

From Coq Require Import Unicode.Utf8.
From Coq Require Import String.
From Coq Require Import List.

Import ListNotations.
Open Scope string.

...etc...

I have had also to fix a missing semicolon here:

Definition Point :=
  class "Point"
    [("x", anum 0); ("y", anum 0)]  (* <- semicolon in list *)
    [
      method "move" [
        assignment "x" (aplus (avar "x") (anum 1));
        assignment "y" (aplus (avar "y") (anum 1))
      ]
    ].

Now it compiles...