X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fdoc%2Fligature.sty;fp=helm%2Focaml%2Ftactics%2Fdoc%2Fligature.sty;h=a914d91d1cad366b87235e7ecbf4814b2230f24d;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hp=0000000000000000000000000000000000000000;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953;p=helm.git

diff --git a/helm/ocaml/tactics/doc/ligature.sty b/helm/ocaml/tactics/doc/ligature.sty
new file mode 100644
index 000000000..a914d91d1
--- /dev/null
+++ b/helm/ocaml/tactics/doc/ligature.sty
@@ -0,0 +1,169 @@
+%%
+%% This is file `ligature.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% semantic.dtx  (with options: `allOptions,ligature')
+%% 
+%% IMPORTANT NOTICE:
+%% 
+%% For the copyright see the source file.
+%% 
+%% Any modified versions of this file must be renamed
+%% with new filenames distinct from ligature.sty.
+%% 
+%% For distribution of the original source see the terms
+%% for copying and modification in the file semantic.dtx.
+%% 
+%% This generated file may be distributed as long as the
+%% original source files, as listed above, are part of the
+%% same distribution. (The sources need not necessarily be
+%% in the same archive or directory.)
+%%
+%% semantic.dtx  (c)1995--2002 Peter M^^f8ller Neergaard and
+%%                             Arne John Glenstrup
+%%
+\expandafter\ifx\csname sem@nticsLoader\endcsname\relax
+  \PackageError{semantic}{%
+    This file should not be loaded directly}
+    {%
+      This file is an option of the semantic package.  It should not be
+        loaded directly\MessageBreak
+      but by using \protect\usepackage{semantic} in your document
+        preamble.\MessageBreak
+      No commands are defined.\MessageBreak
+     Type <return> to proceed.
+    }%
+\else
+\TestForConflict{\@addligto,\@addligtofollowlist,\@def@ligstep}
+\TestForConflict{\@@trymathlig,\@defactive,\@defligstep}
+\TestForConflict{\@definemathlig,\@domathligfirsts,\@domathligfollows}
+\TestForConflict{\@exitmathlig,\@firstmathligs,\@ifactive,\@ifcharacter}
+\TestForConflict{\@ifinlist,\@lastvalidmathlig,\@mathliglink}
+\TestForConflict{\@mathligredefactive,\@mathligsoff,\@mathligson}
+\TestForConflict{\@seentoks,\@setupfirstligchar,\@try@mathlig}
+\TestForConflict{\@trymathlig,\if@mathligon,\mathlig,\mathligprotect}
+\TestForConflict{\mathligsoff,\mathligson,\@startmathlig,\@pushedtoks}
+\newif\if@mathligon
+\DeclareRobustCommand\mathlig[1]{\@addligtolists#1\@@
+  \if@mathligon\mathligson\fi
+  \@setupfirstligchar#1\@@
+  \@defligstep{}#1\@@}
+\def\@mathligson{\if@mathligon\mathligson\fi}
+\def\@mathligsoff{\if@mathligon\mathligsoff\@mathligontrue\fi}
+\DeclareRobustCommand\mathligprotect[1]{\expandafter
+  \def\expandafter#1\expandafter{%
+    \expandafter\@mathligsoff#1\@mathligson}}
+\DeclareRobustCommand\mathligson{\def\do##1##2##3{\mathcode`##1="8000}%
+  \@domathligfirsts\@mathligontrue}
+\AtBeginDocument{\mathligson}
+\DeclareRobustCommand\mathligsoff{\def\do##1##2##3{\mathcode`##1=##2}%
+  \@domathligfirsts\@mathligonfalse}
+\edef\@mathliglink{Error: \noexpand\verb|\string\@mathliglink| expanded}
+{\catcode`\A=11\catcode`\1=12\catcode`\~=13 % Letter, Other and Active
+\gdef\@ifcharacter#1{\ifcat A\noexpand#1\let\next\@firstoftwo
+                \else\ifcat 1\noexpand#1\let\next\@firstoftwo
+                \else\ifcat \noexpand~\noexpand#1\let\next\@firstoftwo
+                \else\let\next\@secondoftwo\fi\fi\fi\next}%
+\gdef\@ifactive#1{\ifcat \noexpand~\noexpand#1\let\next\@firstoftwo
+                  \else\let\next\@secondoftwo\fi\next}}
+\def\@domathligfollows{}\def\@domathligfirsts{}
+\def\@makemathligsactive{\mathligson
+  \def\do##1##2##3{\catcode`##1=12}\@domathligfollows}
+\def\@makemathligsnormal{\mathligsoff
+  \def\do##1##2##3{\catcode`##1=##3}\@domathligfollows}
+\def\@ifinlist#1#2{\@tempswafalse
+  \def\do##1##2##3{\ifnum`##1=`#2\relax\@tempswatrue\fi}#1%
+  \if@tempswa\let\next\@firstoftwo\else\let\next\@secondoftwo\fi\next}
+\def\@addligto#1#2{%
+  \@ifinlist#1#2{\def\do##1##2##3{\noexpand\do\noexpand##1%
+      \ifnum`##1=`#2 {\the\mathcode`#2}{\the\catcode`#2}%
+      \else{##2}{##3}\fi}%
+    \edef#1{#1}}%
+  {\def\do##1##2##3{\noexpand\do\noexpand##1%
+      \ifnum`##1=`#2 {\the\mathcode`#2}{\the\catcode`#2}%
+      \else{##2}{##3}\fi}%
+    \edef#1{#1\do#2{\the\mathcode`#2}{\the\catcode`#2}}}}
+\def\@addligtolists#1{\expandafter\@addligto
+  \expandafter\@domathligfirsts
+  \csname\string#1\endcsname\@addligtofollowlist}
+\def\@addligtofollowlist#1{\ifx#1\@@\let\next\relax\else
+  \def\next{\expandafter\@addligto
+    \expandafter\@domathligfollows
+    \csname\string#1\endcsname
+    \@addligtofollowlist}\fi\next}
+\def\@defligstep#1#2{\def\@tempa##1{\ifx##1\endcsname
+    \expandafter\endcsname\else
+    \string##1\expandafter\@tempa\fi}%
+  \expandafter\@def@ligstep\csname @mathlig\@tempa#1#2\endcsname{#1#2}}
+\def\@def@ligstep#1#2#3{%
+  \ifx#3\@@
+    \def\next{\def#1}%
+  \else
+    \ifx#1\relax
+      \def\next{\let#1\@mathliglink\@defligstep{#2}#3}%
+    \else
+      \def\next{\@defligstep{#2}#3}%
+    \fi
+  \fi\next}
+\def\@setupfirstligchar#1#2\@@{%
+  \@ifactive{#1}{%
+    \expandafter\expandafter\expandafter\@mathligredefactive
+    \expandafter\string\expandafter#1\expandafter{#1}{#1}}%
+  {\@defactive#1{\@startmathlig #1}\@namedef{@mathlig#1}{#1}}}
+\def\@mathligredefactive#1#2#3{%
+  \def#3{{}\ifmmode\def\next{\@startmathlig#1}\else
+    \def\next{#2}\fi\next}%
+  \@namedef{@mathlig#1}{#2}}
+\def\@defactive#1{\@ifundefined{@definemathlig\string#1}%
+  {\@latex@error{Illegal first character in math ligature}
+    {You can only use \@firstmathligs\space as the first^^J
+      character of a math ligature}}%
+  {\csname @definemathlig\string#1\endcsname}}
+
+{\def\@firstmathligs{}\def\do#1{\catcode`#1=\active
+    \expandafter\gdef\expandafter\@firstmathligs
+    \expandafter{\@firstmathligs\space\string#1}\next}
+  \def\next#1{\expandafter\gdef\csname
+    @definemathlig\string#1\endcsname{\def#1}}
+  \do{"}"\do{@}@\do{/}/\do{(}(\do{)})\do{[}[\do{]}]\do{=}=
+  \do{?}?\do{!}!\do{`}`\do{'}'\do{|}|\do{~}~\do{<}<\do{>}>
+  \do{+}+\do{-}-\do{*}*\do{.}.\do{,},\do{:}:\do{;};}
+\newtoks\@pushedtoks
+\newtoks\@seentoks
+\def\@startmathlig{\def\@lastvalidmathlig{}\@pushedtoks{}%
+  \@seentoks{}\@trymathlig}
+\def\@trymathlig{\futurelet\next\@@trymathlig}
+\def\@@trymathlig{\@ifcharacter\next{\@try@mathlig}{\@exitmathlig{}}}
+\def\@exitmathlig#1{%
+  \expandafter\@makemathligsnormal\@lastvalidmathlig\mathligson
+  \the\@pushedtoks#1}
+\def\@try@mathlig#1{%\typeout{char: #1 catcode: \the\catcode`#1
+  \@ifundefined{@mathlig\the\@seentoks#1}{\@exitmathlig{#1}}%
+  {\expandafter\ifx
+                 \csname @mathlig\the\@seentoks#1\endcsname
+                 \@mathliglink
+      \expandafter\@pushedtoks
+        \expandafter=\expandafter{\the\@pushedtoks#1}%
+    \else
+      \expandafter\let\expandafter\@lastvalidmathlig
+      \csname @mathlig\the\@seentoks#1\endcsname
+      \@pushedtoks={}%
+    \fi
+    \expandafter\@seentoks\expandafter=\expandafter%
+    {\the\@seentoks#1}\@makemathligsactive\obeyspaces\@trymathlig}}
+\edef\patch@newmcodes@{%
+  \mathcode\number`\'=39
+  \mathcode\number`\*=42
+  \mathcode\number`\.=\string "613A
+  \mathchardef\noexpand\std@minus=\the\mathcode`\-\relax
+  \mathcode\number`\-=45
+  \mathcode\number`\/=47
+  \mathcode\number`\:=\string "603A\relax
+}
+\AtBeginDocument{\let\newmcodes@=\patch@newmcodes@}
+\fi
+\endinput
+%%
+%% End of file `ligature.sty'.