The Coq mailing list

[Hussain Sobhy <hussain.sob7y AT gmail.com>]

Hello,

I was going through Mike Nahas's tutorial (https://coq.inria.fr/tutorial-nahas) and I came across two examples which I can't get working on CoqIde.

Inductive or (A B:Prop) : Prop :=
  | or_introl : A -> A \/ B
  | or_intror : B -> A \/ B
where "A \/ B" := (or A B) : type_scope.

First Example:

Theorem left_or : (forall A B : Prop, A -> A \/ B).
Proof.
  intros A B.
  intros proof_of_A.
  pose (proof_of_A_or_B := or_introl proof_of_A : A \/ B).
  exact proof_of_A_or_B.
Qed.

Error:
In environment
A, B : Prop
proof_of_A : A
The term "proof_of_A" has type "A"
while it is expected to have type
"Prop".

Second Example:

Theorem right_or : (forall A B : Prop, B -> A \/ B).
Proof.
  intros A B.
  intros proof_of_B.
  refine (or_intror _).
    exact proof_of_B.
Qed.

Error:
In environment
A, B : Prop
proof_of_B : B
The term "or_intror ?P" has type
 "forall B0 : Prop, B0 -> ?P \/ B0"
while it is expected to have type
"A \/ B".

Is it due to the fact that the tutorial used an old version of Coq or is there something fundamentally wrong here?

Thanks,

Hussain