diff options
| author | Guillaume Melquiond | 2016-01-01 23:47:59 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-01-01 23:47:59 +0100 |
| commit | d5b1807e65f7ea29d435c3f894aa551370c5989f (patch) | |
| tree | 48abae07dd6bb1087bc2cdd4a29d74a7419df350 /kernel/uGraph.ml | |
| parent | 53d109a21d97d073bc6a1f36a6c39b940a55eb69 (diff) | |
Fix typos.
Diffstat (limited to 'kernel/uGraph.ml')
| -rw-r--r-- | kernel/uGraph.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 925b2248d8..6765f91ee1 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 |