I'm going crazy but my Coq compiler now is not allowing for inductive propositions as:

Inductive relation : nat -> nat -> Prop :=
  | A : relation 1 2
  | B : relation 2 3.

Throws: Error: The reference B was not found in the current environment.

Inductive le : nat -> nat -> Prop :=
  | le_n (n : nat) : le n n
  | le_S (n m : nat) : le n m -> le n (S m).

Throws: Error: The reference m was not found in the current environment.

My previously running code is not breaking in all the ind. propositions. I don't know if something changed, I'm running these versions:

The Coq Proof Assistant, version 8.18.0
compiled with OCaml 5.1.0

Any ideas?

If I use only one rule as:

Inductive relation : nat -> nat -> Prop :=
  | A : relation 1 2.

Works. So I tried changing from tabs to spaces. I didn't change the Coq version because this is the version that was actually compiling some days ago.