The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Is it possible to overwrite existing [Coercion]s?  For example, is there a way to override the coercions in Coq.Init.Specif between [sig] and [sigT] so that something like the following will work?

Set Printing Coercions.

Definition sig_of_sigT (A : Type) (P : A -> Prop) (X : sigT P) : sig P

  := exist P (projT1 X) (projT2 X).

Definition sigT_of_sig (A : Type) (P : A -> Prop) (X : sig P) : sigT P

  := existT P (proj1_sig X) (proj2_sig X).

Coercion sigT_of_sig : sig >-> sigT.

Coercion sig_of_sigT : sigT >-> sig.

Goal (fun A (P : A -> Prop) (X : sigT P) => proj1_sig X) = (fun A (P : A -> Prop) (X : sigT P) => projT1 X).

  (* Note the [Specif.sig_of_sigT].  I want it to be [sig_of_sigT]. *)

  reflexivity.

Qed.

Thanks,

Jason