diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-08 17:11:59 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-08 17:11:59 +0000 |
| commit | b0b1710ba631f3a3a3faad6e955ef703c67cb967 (patch) | |
| tree | 9d35a8681cda8fa2dc968535371739684425d673 /plugins | |
| parent | bafb198e539998a4a64b2045a7e85125890f196e (diff) | |
Monomorphized a lot of equalities over OCaml integers, thanks to
the new Int module. Only the most obvious were removed, so there
are a lot more in the wild.
This may sound heavyweight, but it has two advantages:
1. Monomorphization is explicit, hence we do not miss particular
optimizations of equality when doing it carelessly with the generic
equality.
2. When we have removed all the generic equalities on integers, we
will be able to write something like "let (=) = ()" to retrieve all
its other uses (mostly faulty) spread throughout the code, statically.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
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 a811b29b8..485b5b280 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 beb7b4819..d42d612ae 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 d9201722d..571c789c2 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 1f7c083e2..339e10661 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) |