Coq

At this moment I am just trying to run the code in the Coq Tutorial...

The following e-script, corresponding to the section "Existential Quantification" of the tutorial, is not working as it should:

*;; (find-coqv81w3m "tutorial.html#htoc12" "Sections and signatures")
* (eepitch-coqtop)
* (eepitch-kill)
* (eepitch-coqtop)
Reset Initial.
Section Predicate_calculus.
Variable D : Set.
Variable R : D -> D -> Prop.
Section R_sym_trans.
Hypothesis R_symmetric : forall x y:D, R x y -> R y x.
Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z.
Lemma refl_if : forall x:D, (exists y, R x y) -> R x x.
Check ex.
intros x x_Rlinked.
intro y.

Here is its log:

Welcome to Coq 8.1pl3 (Dec. 2007)

Coq < Reset Initial.

Coq < Section Predicate_calculus.

Coq < Variable D : Set.
D is assumed

Coq < Variable R : D -> D -> Prop.
R is assumed

Coq < Section R_sym_trans.

Coq < Hypothesis R_symmetric : forall x y:D, R x y -> R y x.
R_symmetric is assumed

Coq < Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z.
R_transitive is assumed

Coq < Lemma refl_if : forall x:D, (exists y, R x y) -> R x x.
1 subgoal
  
  D : Set
  R : D -> D -> Prop
  R_symmetric : forall x y : D, R x y -> R y x
  R_transitive : forall x y z : D, R x y -> R y z -> R x z
  ============================
   forall x : D, (exists y : D, R x y) -> R x x

refl_if < Check ex.
ex
     : forall A : Type, (A -> Prop) -> Prop

refl_if < intros x x_Rlinked.
1 subgoal
  
  D : Set
  R : D -> D -> Prop
  R_symmetric : forall x y : D, R x y -> R y x
  R_transitive : forall x y z : D, R x y -> R y z -> R x z
  x : D
  x_Rlinked : exists y : D, R x y
  ============================
   R x x

refl_if < intro y.
Toplevel input, characters 0-7
> intro y.
> ^^^^^^^
User error: No product even after head-reduction

refl_if <