aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/libtypes.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/libtypes.mli')
-rw-r--r--toplevel/libtypes.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli
index be5e9312a..d57ecb948 100644
--- a/toplevel/libtypes.mli
+++ b/toplevel/libtypes.mli
@@ -12,8 +12,8 @@
open Term
(*i*)
-(*
- * Persistent library of all declared object,
+(*
+ * Persistent library of all declared object,
* indexed by their types (uses Dnets)
*)
@@ -24,7 +24,7 @@ type result = Libnames.global_reference * (constr*existential_key) * Termops.sub
(* this is the reduction function used in the indexing process *)
val reduce : types -> types
-(* The different types of search available.
+(* The different types of search available.
* See term_dnet.mli for more explanations *)
val search_pattern : types -> result list
val search_concl : types -> result list