From e41d7212c8c768f21a2baf61bb174a57bb7438a1 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 20 Mar 2008 20:56:29 +0000
Subject: Add a flag to control rewriting under lambdas. Otherwise makes some
 rewrite calls fail because an occurence is found under a lambda that was not
 found before and there are no adequate morphism declarations to make the
 rewrite succeed nor the possibility to give occurences to rewrite (yet). Only
 setoid_rewrite will try rewriting under lambda's for now. Example problem
 found in a port of the Random library. Also improved the required_library
 error message.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10704 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Basics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index d6c276d16a..1129c5b65e 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -21,11 +21,11 @@ Definition id {A} := fun x : A => x.
 
 (** Function composition. *)
 
-Definition compose {A B C} (f : A -> B) (g : B -> C) := fun x : A => g (f x).
+Definition compose {A B C} (g : B -> C) (f : A -> B) := fun x : A => g (f x).
 
 Hint Unfold compose.
 
-Notation " g ∘ f " := (compose f g)  (at level 50, left associativity) : program_scope.
+Notation " g ∘ f " := (compose g f)  (at level 50, left associativity) : program_scope.
 
 Open Local Scope program_scope.
 
-- 
cgit v1.2.3