From b48240e2c319eb66be3b58d3812792e86be56d32 Mon Sep 17 00:00:00 2001 From: narboux Date: Fri, 30 Apr 2004 11:18:39 +0000 Subject: les accents sont ok git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8559 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/newfaq/main.tex | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex index 4a816b5e4..f78947c5f 100644 --- a/doc/newfaq/main.tex +++ b/doc/newfaq/main.tex @@ -1,4 +1,3 @@ - \documentclass[a4paper]{article} \pagestyle{plain} @@ -6,11 +5,11 @@ \usepackage{stmaryrd} \usepackage{amssymb} \usepackage{url} -\usepackage{multicol} +%\usepackage{multicol} \usepackage{hevea} \usepackage{fullpage} -%\usepackage[latin1]{inputenc} -%\usepackage[english]{babel} +\usepackage[latin1]{inputenc} +\usepackage[english]{babel} %\input{../macros.tex} @@ -1773,15 +1772,16 @@ You can use this bibtex entry : \Question{How to use those Forall and Exists pretty symbols ?}\label{forallcoqide} Thanks to the notation features in \Coq, you just need to insert these -lines in your \Coq buffer : +lines in your \Coq buffer :\\ \begin{texttt} -======================================================================\\ Notation "$\forall$ x : t, P" := (forall x:t, P) (at level 200, x ident). +\end{texttt}\\ +\begin{texttt} Notation "$\exists$ x : t, P" := (exists x:t, P) (at level 200, x ident). -====================================================================== \end{texttt} + Copy/Paste of these lines from this file will not work outside of \CoqIde. -You need to load a file containing these lines or to enter the "∀" +You need to load a file containing these lines or to enter the $\forall$ using an input method (see \ref{inputmeth}). To try it just use \verb#Require utf8# from inside \CoqIde. To enable these notations automatically start coqide with @@ -1795,7 +1795,7 @@ pretty simple notations. \begin{itemize} \item First solution : type \verb#2200# to enter a forall in the script widow. - 2200 is the hexadecimal code for forall in unicode charts and is encoded as "∀" + 2200 is the hexadecimal code for forall in unicode charts and is encoded as in UTF-8. 2203 is for exists. See \url{http://www.unicode.org} for more codes. \item Second solution : rebind \verb#a# to forall and \verb#e# to exists. @@ -1806,11 +1806,11 @@ pretty simple notations. \end{verbatim} and then to add \begin{verbatim} - bind "F13" {"insert-at-cursor" ("∀")} - bind "F14" {"insert-at-cursor" ("∃")} + bind "F13" {"insert-at-cursor" ("")} + bind "F14" {"insert-at-cursor" ("")} \end{verbatim} to your "binding "text"" section in \verb#.coqiderc-gtk2rc.# - The strange ("∀") argument is the UTF-8 encoding for + The strange ("") argument is the UTF-8 encoding for 0x2200. You can compute these encodings using the lablgtk2 toplevel with \begin{verbatim} -- cgit v1.2.3