From ac93dc5cf57cb28bfb843baf96f3f9e7e6e0318a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 22 Jul 2010 08:04:19 +0000 Subject: [PATCH] fixed precedence so that no () are needed around variable assignement --- helm/software/matita/nlibrary/hints_declaration.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/nlibrary/hints_declaration.ma b/helm/software/matita/nlibrary/hints_declaration.ma index f91949be9..27330da46 100644 --- a/helm/software/matita/nlibrary/hints_declaration.ma +++ b/helm/software/matita/nlibrary/hints_declaration.ma @@ -37,7 +37,7 @@ With unidoce and some ASCII art it looks like the following: *) (* it seems unbelivable, but it works! *) -notation > "≔ (list0 ( (list1 (ident x) sep , ) opt (: T) ) sep ,) opt (; (list1 (ident U ≟ term 90 V ) sep ,)) ⊢ term 19 Px ≡ term 19 Py" +notation > "≔ (list0 ( (list1 (ident x) sep , ) opt (: T) ) sep ,) opt (; (list1 (ident U ≟ term 19 V ) sep ,)) ⊢ term 19 Px ≡ term 19 Py" with precedence 90 for @{ ${ fold right @{ ${ default -- 2.39.2