From 876b1b39a0304c93c2511ca8dd34353413e91c9d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 12 Aug 2014 11:03:05 -0400 Subject: instanciation is French, instantiation is English --- theories/Classes/Morphisms_Relations.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Classes') diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v index dc46b4bbb..44e4808b8 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -38,7 +38,7 @@ Lemma predicate_implication_pointwise (l : Tlist) : Proper (@predicate_implication l ==> pointwise_lifting impl l) id. Proof. do 2 red. unfold predicate_implication. auto. Qed. -(** The instanciation at relation allows to rewrite applications of relations +(** The instantiation at relation allows to rewrite applications of relations [R x y] to [R' x y] when [R] and [R'] are in [relation_equivalence]. *) Instance relation_equivalence_pointwise : -- cgit v1.2.3