Skip to content
Snippets Groups Projects
Commit 730c2860 authored by David Swasey's avatar David Swasey Committed by Ralf Jung
Browse files

Protect resp_set from SSR.

parent 9c413c19
No related branches found
No related tags found
No related merge requests found
......@@ -34,7 +34,7 @@ Arguments morph_resp [S T eqS eqT] _ _ _ _.
Infix "-=>" := morphism (at level 45, right associativity).
Notation "'s[(' f ')]'" := (mkMorph f _).
Ltac resp_set :=
intros t1 t2 HEqt; repeat (intros ?); simpl in *; try rewrite !HEqt; reflexivity.
intros t1 t2 HEqt; repeat (intros ?); simpl in *; try rewrite -> !HEqt; reflexivity.
(** This seems just to be a package putting together all the
ingredients of [type], i.e. the carrier set, the relation and the
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment