From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- test-suite/bugs/closed/HoTT_coq_077.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/bugs/closed/HoTT_coq_077.v') diff --git a/test-suite/bugs/closed/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v index db3b60ed..017780c1 100644 --- a/test-suite/bugs/closed/HoTT_coq_077.v +++ b/test-suite/bugs/closed/HoTT_coq_077.v @@ -30,7 +30,7 @@ Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B) (p : prod A B) : P p := u (fst p) (snd p). -Notation typeof x := ($(let T := type of x in exact T)$) (only parsing). +Notation typeof x := (ltac:(let T := type of x in exact T)) (only parsing). (* Check for eta *) Check eq_refl : typeof (@prod_rect) = typeof (@prod_rect'). -- cgit v1.2.3