diff options
| author | Maxime Dénès | 2018-09-26 14:55:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-26 14:55:29 +0200 |
| commit | 5ced288419aed8a622ed2c267e35d9a174facafc (patch) | |
| tree | 2b4f617546ff718e2acad62d35fd7cf3f6d6467a /kernel/uGraph.ml | |
| parent | 871c694e5395e85296f4c61ba4039f04704b20b3 (diff) | |
| parent | 2cceef0e3cab18b1dcc28bf1c8ce6b4723cd3d9a (diff) | |
Merge PR #7571: [kernel] Compile with almost all warnings enabled.
Diffstat (limited to 'kernel/uGraph.ml')
| -rw-r--r-- | kernel/uGraph.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 95d71965df..9ff51fca55 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -194,7 +194,7 @@ let check_universes_invariants g = UMap.iter (fun l u -> match u with | Canonical u -> - UMap.iter (fun v strict -> + UMap.iter (fun v _strict -> incr n_edges; let v = repr g v in assert (topo_compare u v = -1); @@ -435,7 +435,7 @@ let reorder g u v = | n0::q0 -> (* Computing new root. *) let root, rank_rest = - List.fold_left (fun ((best, rank_rest) as acc) n -> + List.fold_left (fun ((best, _rank_rest) as acc) n -> if n.rank >= best.rank then n, best.rank else acc) (n0, min_int) q0 in @@ -809,7 +809,7 @@ let normalize_universes g = in UMap.fold (fun _ u g -> match u with - | Equiv u -> g + | Equiv _u -> g | Canonical u -> let _, u, g = get_ltle g u in let _, _, g = get_gtge g u in @@ -821,7 +821,7 @@ let constraints_of_universes g = let uf = UF.create () in let constraints_of u v acc = match v with - | Canonical {univ=u; ltle} -> + | Canonical {univ=u; ltle; _} -> UMap.fold (fun v strict acc-> let typ = if strict then Lt else Le in Constraint.add (u,typ,v) acc) ltle acc @@ -943,7 +943,7 @@ let check_eq_instances g t1 t2 = (** Pretty-printing *) let pr_arc prl = function - | _, Canonical {univ=u; ltle} -> + | _, Canonical {univ=u; ltle; _} -> if UMap.is_empty ltle then mt () else prl u ++ str " " ++ @@ -963,7 +963,7 @@ let pr_universes prl g = let dump_universes output g = let dump_arc u = function - | Canonical {univ=u; ltle} -> + | Canonical {univ=u; ltle; _} -> let u_str = Level.to_string u in UMap.iter (fun v strict -> let typ = if strict then Lt else Le in |