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.

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.

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 shomething changed, I'm runnig this 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.

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.