From 07e03e167c7eda30ffc989530470b5c597beaedc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 15 Apr 2008 12:00:50 +0000
Subject: - Un peu de doc, préparation du CHANGES pour la release. -
 Re-restriction de inversion (après la correction des bugs - et   notamment du
 "Unknown meta" qui apparaissait parfois -, inversion   devenait capable
 d'agir sur des buts non atomiques, ce qui crée   quelques incompatibilités,
 typiquement dans CoRN où inversion est   utilisé dans un rôle de
 discriminate; en attendant de voir, on   revient à la sémantique initiale). -
 Généralisation de Local/Global dans Implicit Arguments pour avoir un  
 fonctionnement plus uniforme et plus facile à documenter. - Code mort
 (clenv.ml).

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

(limited to 'doc/common')

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 47409b9845..3bfe09c166 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -213,6 +213,7 @@
 \newcommand{\onemodbinding}{\textrm{\textsl{module\_binding}}}
 \newcommand{\modbindings}{\textrm{\textsl{module\_bindings}}}
 \newcommand{\qualid}{\textrm{\textsl{qualid}}}
+\newcommand{\qualidorstring}{\textrm{\textsl{qualid\_or\_string}}}
 \newcommand{\class}{\textrm{\textsl{class}}}
 \newcommand{\dirpath}{\textrm{\textsl{dirpath}}}
 \newcommand{\typedidents}{\textrm{\textsl{typed\_idents}}}
-- 
cgit v1.2.3