aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorMaxime Dénès2018-12-12 09:57:09 +0100
committerMaxime Dénès2018-12-12 09:57:09 +0100
commitd87c4c472478fbcb30de6efabc68473ee36849a1 (patch)
tree5b4e1cb66298db57b978374422822ffdf2673100 /tools
parent850dfbf59f52b0d3dcba237ee2af5ce99fd1bcd2 (diff)
parentd00472c59d15259b486868c5ccdb50b6e602a548 (diff)
Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdep.ml4
-rw-r--r--tools/coqdep_common.ml2
2 files changed, 3 insertions, 3 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 226a19678f..4e80caa4cc 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -233,7 +233,7 @@ struct
let rem = NSet.fold push next rem in
aux rem seen
| Some false ->
- (** The path we took encountered x -> y but not the one in seen *)
+ (* The path we took encountered x -> y but not the one in seen *)
if through then aux (NMap.add n true rem) (NMap.add n true seen)
else aux rem seen
| Some true -> aux rem seen
@@ -357,7 +357,7 @@ let treat_coq_file chan =
| None -> acc
| Some file_str -> (canonize file_str, ".v") :: acc
else acc
- | AddLoadPath _ | AddRecLoadPath _ -> acc (** TODO *)
+ | AddLoadPath _ | AddRecLoadPath _ -> acc (* TODO *)
in
loop acc
in
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index db2031c64b..e3dd32fb63 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -132,7 +132,7 @@ let add_mllib_known, _, search_mllib_known = mkknown ()
let add_mlpack_known, _, search_mlpack_known = mkknown ()
let vKnown = (Hashtbl.create 19 : (string list, string * bool) Hashtbl.t)
-(** The associated boolean is true if this is a root path. *)
+(* The associated boolean is true if this is a root path. *)
let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t)
let get_prefix p l =