diff options
| -rw-r--r-- | engine/universes.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tauto.ml | 2 | ||||
| -rw-r--r-- | tactics/term_dnet.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index ad5ff827bd..ab561784c3 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 ++ diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index dc7ee6a234..e86d1c7283 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -242,7 +242,7 @@ let tauto_uniform_unit_flags = { } (* This is the compatibility mode (not used) *) -let tauto_legacy_flags = { +let _tauto_legacy_flags = { binary_mode = true; binary_mode_bugged_detection = true; strict_in_contravariant_hyp = true; diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 2c863c42a6..726fd23b64 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -49,7 +49,7 @@ struct | DNil (* debug *) - let pr_dconstr f : 'a t -> std_ppcmds = function + let _pr_dconstr f : 'a t -> std_ppcmds = function | DRel -> str "*" | DSort -> str "Sort" | DRef _ -> str "Ref" |