From cd3be69adce23c812c968ed33ecb6ea8b43ef2ab Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 10 Mar 2000 17:49:33 +0000 Subject: t -> $t dans regle grammaire EX git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@313 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Init/LogicSyntax.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Init/LogicSyntax.v') diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v index b0e8bd5ba..50bed8827 100644 --- a/theories/Init/LogicSyntax.v +++ b/theories/Init/LogicSyntax.v @@ -42,7 +42,7 @@ with constr10 := | eximplicit [ "EX" ident($v) "|" constr($c1) ] -> [<<(ex ? [$v]$c1)>>] | ex2explicit [ "EX" ident($v) ":" constr($t) "|" constr($c1) "&" - constr($c2) ] -> [<<(ex2 $t [$v : $t]$c1 [$v : t]$c2)>>] + constr($c2) ] -> [<<(ex2 $t [$v : $t]$c1 [$v : $t]$c2)>>] | ex2implicit [ "EX" ident($v) "|" constr($c1) "&" constr($c2) ] -> [<<(ex2 ? [$v]$c1 [$v]$c2)>>]. -- cgit v1.2.3