aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/uGraph.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-01 23:47:59 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-01 23:47:59 +0100
commitd5b1807e65f7ea29d435c3f894aa551370c5989f (patch)
tree48abae07dd6bb1087bc2cdd4a29d74a7419df350 /kernel/uGraph.ml
parent53d109a21d97d073bc6a1f36a6c39b940a55eb69 (diff)
Fix typos.
Diffstat (limited to 'kernel/uGraph.ml')
-rw-r--r--kernel/uGraph.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 925b2248d..6765f91ee 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -277,7 +277,7 @@ exception CycleDetected
problems. arXiv preprint arXiv:1112.0784. *)
(* [delta] is the timeout for backward search. It might be
- usefull to tune a multiplicative constant. *)
+ useful to tune a multiplicative constant. *)
let get_delta g =
int_of_float
(min (float_of_int g.n_edges ** 0.5)
@@ -668,7 +668,7 @@ let check_leq g u v =
is_type0m_univ u ||
check_eq_univs g u v || real_check_leq g u v
-(* enforc_univ_eq g u v will force u=v if possible, will fail otherwise *)
+(* enforce_univ_eq g u v will force u=v if possible, will fail otherwise *)
let rec enforce_univ_eq u v g =
let ucan = repr g u in