From 528c237b658dbba896a1fe0041990cc7fec9c4c8 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:07:32 +0200
Subject: Add [_] prefix to unused values which maybe should be kept

---
 engine/universes.ml   | 2 +-
 plugins/ltac/tauto.ml | 2 +-
 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"
-- 
cgit v1.2.3