diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-21 20:07:32 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:39:25 +0200 |
| commit | 528c237b658dbba896a1fe0041990cc7fec9c4c8 (patch) | |
| tree | d10056965de5b7981039134fc99009ad98bdacb8 /engine/universes.ml | |
| parent | 02d2f34e5c84f0169e884c07054a6fbfef9f365c (diff) | |
Add [_] prefix to unused values which maybe should be kept
Diffstat (limited to 'engine/universes.ml')
| -rw-r--r-- | engine/universes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index ad5ff827b..ab561784c 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -732,7 +732,7 @@ let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cs type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t -let pr_constraints_map cmap = +let _pr_constraints_map (cmap:constraints_map) = LMap.fold (fun l cstrs acc -> Level.pr l ++ str " => " ++ prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ |