diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/merge.ml | 2 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 2 | ||||
| -rw-r--r-- | plugins/micromega/mfourier.ml | 4 | ||||
| -rw-r--r-- | plugins/micromega/polynomial.ml | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index a811b29b84..485b5b2808 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -227,7 +227,7 @@ let linkmonad f lnkvar = let linklift lnkvar i = linkmonad (fun x -> x+i) lnkvar (* This map is used to deal with debruijn linked indices. *) -module Link = Map.Make (struct type t = int let compare = Pervasives.compare end) +module Link = Map.Make (Int) let pr_links l = Printf.printf "links:\n"; diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index beb7b4819c..d42d612ae5 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -243,7 +243,7 @@ let rec add_term t0 = function * MODULE: Ordered set of integers. *) -module ISet = Set.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end) +module ISet = Set.Make(Int) (** * Given a set of integers s={i0,...,iN} and a list m, return the list of diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index d9201722d6..571c789c29 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -89,7 +89,7 @@ type vector = Vect.t {coeffs = v ; bound = (l,r) } models the constraints l <= v <= r **) -module ISet = Set.Make(struct type t = int let compare = Pervasives.compare end) +module ISet = Set.Make(Int) module PSet = ISet @@ -437,7 +437,7 @@ let elim_var_using_eq vr vect cst prf sys = (** [size sys] computes the number of entries in the system of constraints *) let size sys = System.fold (fun v iref s -> s + (!iref).neg + (!iref).pos) sys 0 -module IMap = Map.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end) +module IMap = Map.Make(Int) let pp_map o map = IMap.fold (fun k elt () -> Printf.fprintf o "%i -> %s\n" k (string_of_num elt)) map () diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index 1f7c083e22..339e106619 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -585,7 +585,7 @@ struct module MonT = struct module MonoMap = Map.Make(Monomial) - module IntMap = Map.Make(struct type t = int let compare = Pervasives.compare end) + module IntMap = Map.Make(Int) (** A hash table might be preferable but requires a hash function. *) let (index_of_monomial : int MonoMap.t ref) = ref (MonoMap.empty) |