From 30c687b1fd0d2d9d3299f71971dc230cdd042e79 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 6 Feb 2008 18:23:36 +0000
Subject: - Documentation des nouvelles options d'implicites (Set Strongly
 Strict   Implicit, Set Maximal Implicit Insertion, Set Reversible Pattern  
 Implicit, Set Printing Implicit Defensive). - Changement de la sémantique de
 Set Strongly Strict Implicit : il   contient maintenant Set Strict Implicit.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10520 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 6cbd06eae2..47409b9845 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -172,6 +172,7 @@
 \newcommand{\localdecls}{\textrm{\textsl{local\_decls}}}
 \newcommand{\ident}{\textrm{\textsl{ident}}}
 \newcommand{\accessident}{\textrm{\textsl{access\_ident}}}
+\newcommand{\possiblybracketedident}{\textrm{\textsl{possibly\_bracketed\_ident}}}
 \newcommand{\inductivebody}{\textrm{\textsl{ind\_body}}}
 \newcommand{\inductive}{\textrm{\textsl{inductive}}}
 \newcommand{\naturalnumber}{\textrm{\textsl{natural}}}
-- 
cgit v1.2.3