From ec09e6b0d0894e926f1b26afbd033e106101e8ac Mon Sep 17 00:00:00 2001
From: mohring
Date: Fri, 19 Dec 2003 12:39:57 +0000
Subject: v8/CIC

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8420 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/macros.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/macros.tex b/doc/macros.tex
index 3b3417ed2f..d85a9601e3 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -337,8 +337,8 @@
 \newcommand{\Def}[4]{\mbox{{\sf Def}$(#1)(#2:=#3:#4)$}}
 \newcommand{\Assum}[3]{\mbox{{\sf Assum}$(#1)(#2:#3)$}}
 \newcommand{\Match}[3]{\mbox{$<\!#1\!>\!{\mbox{\tt Match}}~#2~{\mbox{\tt with}}~#3~{\mbox{\tt end}}$}}
-\newcommand{\Case}[3]{\mbox{$\kw{match}~#2~\kw{return}~#1~\kw{with}~#3~
-\kw{end}$}}
+\newcommand{\Case}[3]{\mbox{$\kw{case}(#2,#1,#3)$}}
+\newcommand{\match}[3]{\mbox{$\kw{match}~ #2 ~\kw{with}~ #3 ~\kw{end}$}}
 \newcommand{\Fix}[2]{\mbox{\tt Fix}~#1\{#2\}}
 \newcommand{\CoFix}[2]{\mbox{\tt CoFix}~#1\{#2\}}
 \newcommand{\With}[2]{\mbox{\tt ~with~}}
-- 
cgit v1.2.3