From 0b6924f05ef6beb775345f3fb2ad21a009ab3baa Mon Sep 17 00:00:00 2001 From: msozeau Date: Sat, 29 Mar 2008 11:20:45 +0000 Subject: Fix test-suite files, change conflicting notation "->rel" and the others to "-R>" and the like. Split more precisely in inference of case predicate between the new code which currently works only for matched variables and the old one which works better on variables appearing in matched terms types (the two could also be merged). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10729 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/success/LetPat.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'test-suite/success/LetPat.v') diff --git a/test-suite/success/LetPat.v b/test-suite/success/LetPat.v index 72c7cc155..545b8aeb8 100644 --- a/test-suite/success/LetPat.v +++ b/test-suite/success/LetPat.v @@ -48,8 +48,8 @@ Definition identity_functor (c : category) : functor c c := fun x => x. Definition functor_composition (a b c : category) : functor a b -> functor b c -> functor a c := - let ' (A :& homA :& CA) := a in - let ' (B :& homB :& CB) := b in - let ' (C :& homB :& CB) := c in + let 'A :& homA :& CA := a in + let 'B :& homB :& CB := b in + let 'C :& homB :& CB := c in fun f g => - fun x : A => g (f x). + fun x => g (f x). -- cgit v1.2.3