diff options
| author | herbelin | 2005-11-08 17:14:52 +0000 |
|---|---|---|
| committer | herbelin | 2005-11-08 17:14:52 +0000 |
| commit | 4a7555cd875b0921368737deed4a271450277a04 (patch) | |
| tree | ea296e097117b2af5606e7365111f5694d40ad9a /lib | |
| parent | 8d94b3c7f4c51c5f78e6438b7b3e39f375ce9979 (diff) | |
Nettoyage suite à la détection par défaut des variables inutilisées par ocaml 3.09
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/gmap.ml | 4 | ||||
| -rw-r--r-- | lib/pp.ml4 | 1 | ||||
| -rw-r--r-- | lib/profile.ml | 6 |
3 files changed, 5 insertions, 6 deletions
diff --git a/lib/gmap.ml b/lib/gmap.ml index 989c8f22d7..4febb3ad1d 100644 --- a/lib/gmap.ml +++ b/lib/gmap.ml @@ -57,7 +57,7 @@ let rec add x data = function Empty -> Node(Empty, x, data, Empty, 1) - | Node(l, v, d, r, h) as t -> + | Node(l, v, d, r, h) -> let c = Pervasives.compare x v in if c = 0 then Node(l, x, data, r, h) @@ -91,7 +91,7 @@ let rec remove x = function Empty -> Empty - | Node(l, v, d, r, h) as t -> + | Node(l, v, d, r, h) -> let c = Pervasives.compare x v in if c = 0 then merge l r diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 7f0def5293..91a99b5fbd 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -183,7 +183,6 @@ let rec pr_com ft s = (* pretty printing functions *) let pp_dirs ft = - let maxbox = (get_gp ft).max_depth in let pp_open_box = function | Pp_hbox n -> Format.pp_open_hbox ft () | Pp_vbox n -> Format.pp_open_vbox ft n diff --git a/lib/profile.ml b/lib/profile.ml index 1197c92a91..80ae6b4b45 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -259,9 +259,9 @@ let time_overhead_B_C () = for i=1 to loops do try dummy_last_alloc := get_alloc (); - let r = dummy_f dummy_x in - let dw = dummy_spent_alloc () in - let dt = get_time () in + let _r = dummy_f dummy_x in + let _dw = dummy_spent_alloc () in + let _dt = get_time () in () with _ -> assert false done; |