The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

While trying to compile Ynot, in Axioms.v, theorem Dyn_inj, I had an error  
on injection 1.

I succeed in repairing it in the file


Theorem Dyn_inj : forall (T : Set) (x y : T),
  Dyn x = Dyn y
  -> x = y.
 set (pi := fun (X : dynamic) =>
      match X with
      | Dyn T t => existT (fun t : Type => t) T t
      end).
 intros; assert (pi (Dyn x) = pi (Dyn y)).
  case H; split.
 clear H; subst pi; simpl in H0.
 exact (inj_pair2 _ _ _ _ _ H0).
Qed.

instead of

Theorem Dyn_inj : forall (T : Set) (x y : T),
  Dyn x = Dyn y
  -> x = y.
 injection 1; intros.
 exact (inj_pair2 _ _ _ _ _ H0).
Qed.

So injection seems to be broken. As I am in trunk, I don't know if I must  
submit a bug report or if it is known and intended to be repaired.

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay