From 81f12192810bdf825cee82658a36214740d1a75b Mon Sep 17 00:00:00 2001
From: soubiran
Date: Fri, 23 May 2008 10:39:50 +0000
Subject: Nouvelle doc pour les modules.

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

(limited to 'doc/common')

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 47baa94a6f..6b6c158b51 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -385,6 +385,8 @@
 
 \newcommand{\Indp}[5]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{@{}l}#3:=#4
                                                  \,)\end{array}$}}
+\newcommand{\Indpstr}[6]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{@{}l}#3:=#4
+                                                 \,)/{#6}\end{array}$}}
 \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}}$}}
@@ -406,7 +408,7 @@
 
 \newcommand{\Impl}{{\it Impl}}
 \newcommand{\elem}{{\it e}}
-\newcommand{\Mod}[3]{{\sf Mod}({#1}:{#2}:={#3})}
+\newcommand{\Mod}[3]{{\sf Mod}({#1}:{#2}\,\zeroone{:={#3}})}
 \newcommand{\ModS}[2]{{\sf Mod}({#1}:{#2})}
 \newcommand{\ModType}[2]{{\sf ModType}({#1}:={#2})}
 \newcommand{\ModA}[2]{{\sf ModA}({#1}=={#2})}
-- 
cgit v1.2.3