diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/genarg.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/genarg.mli b/lib/genarg.mli index bb85f99e3c..52db3df088 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -13,7 +13,7 @@ (** The route of a generic argument, from parsing to evaluation. In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. -{% \begin{%}verbatim{% }%} +{% \begin{verbatim} %} parsing in_raw out_raw char stream ---> raw_object ---> raw_object generic_argument -------+ encapsulation decaps| @@ -36,7 +36,7 @@ In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. | V effective use -{% \end{%}verbatim{% }%} +{% \end{verbatim} %} To distinguish between the uninterpreted, globalized and interpreted worlds, we annotate the type [generic_argument] by a |