The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Hi !

I have the same problem here : it is particularly annoying to rewrite an equality that contains Type instances, if these instances are not the same in the equality and in the goal !

The same problem exists when trying to use all the tactics that search for a subterm in the goal.

Is this a bug or a feature ?

If this is a feature, is there a good work-around ?

--
Jacques-Henri Jourdan

---

De: "Jason Gross" <jasongross9 AT gmail.com>
À: coq-club AT inria.fr
Envoyé: Jeudi 19 Juillet 2012 23:12:50
Objet: [Coq-Club] Variant of [rewrite] that ignores type universes?

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