My Coq compiler 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.