aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-05-24 03:52:06 +0200
committerEmilio Jesus Gallego Arias2018-09-10 10:45:15 +0200
commit42bb3db8c897c5b3c82fcf1d4e4f71ee0e0d2bef (patch)
tree0851ea50e178b12dd1caacbd2ce20ad9cb58572d /lib
parent73c3c7c6b3d35439c58126d0b55cf7a7e3235191 (diff)
[dune] Add apidoc target using `odoc`
We build the `@doc` target in the `dune` job: - The documentation can be found in `_build/default/_doc/` - We had to fix a couple of quoting problems.
Diffstat (limited to 'lib')
-rw-r--r--lib/genarg.mli4
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