aboutsummaryrefslogtreecommitdiff
path: root/kernel/constr.mli
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 /kernel/constr.mli
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 'kernel/constr.mli')
-rw-r--r--kernel/constr.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 70acf19328..8fe77d448e 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -285,8 +285,8 @@ val destMeta : constr -> metavariable
(** Destructs a variable *)
val destVar : constr -> Id.t
-(** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether
- [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *)
+(** Destructs a sort. [is_Prop] recognizes the sort [Prop], whether
+ [isprop] recognizes both [Prop] and [Set]. *)
val destSort : constr -> Sorts.t
(** Destructs a casted term *)