The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is it a known/desired behavior that [rewrite] fails to match [Type]s in different universes?  (I'm using Coq 8.4beta2.)  Is there a way to tell [rewrite] to turn off it's universe strictness?

For example, I have the following code:

Set Printing Universes.

Goal Type = Type.

  pose Type as a.

  assert (H : Type = a) by reflexivity.

  (* rewrite H. (* "Found no subterm matching "Type (* Top.8 *)" in the current goal." *) *)

  match goal with

    | [ H : ?x = _ |- ?x = _ ] => idtac x (* Type (* Top.8 *) *)

  end.

  match goal with

    | [ H : ?x = _ |- ?y = _ ] => let H' := fresh in

      assert (H' : x = y) by reflexivity;

        rewrite <- H'; clear H';

          rewrite H (* succeeds *)

  end.

                                    

Thanks.

-Jason