- 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

1 files changed, 1 insertions, 0 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 6cbd06eae..47409b984 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}}}