From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- theories/Unicode/Utf8_core.v | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) (limited to 'theories/Unicode/Utf8_core.v') diff --git a/theories/Unicode/Utf8_core.v b/theories/Unicode/Utf8_core.v index 44a0700a..5a8931a8 100644 --- a/theories/Unicode/Utf8_core.v +++ b/theories/Unicode/Utf8_core.v @@ -1,19 +1,23 @@ (* -*- coding:utf-8 -*- *) (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* y) (at level 70) : type_scope. (* Abstraction *) -Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) - (at level 200, x binder, y binder, right associativity). +Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' 'λ' x .. y ']' , t"). -- cgit v1.2.3