diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-25 22:34:08 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-25 22:34:08 +0000 |
| commit | f4a6a6aaa928e7a6c8d360c45268cb82c020c2dc (patch) | |
| tree | 95bf369c1f34a6a4c055357b68e60de58849bd11 /plugins | |
| parent | 646c6765e5e3307f8898c4f63c405d91c2e6f47b (diff) | |
Added a more efficient way to recover the domain of a map.
The extended signature is defined in CMap, and should be compatible
with the old one, except that module arguments have to be explicitely
named. The implementation itself is quite unsafe, as it relies on the
current implementation of OCaml maps, even though that should not be
a problem (it has not changed in ages).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 19 | ||||
| -rw-r--r-- | plugins/rtauto/proof_search.ml | 3 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 2 |
3 files changed, 16 insertions, 8 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index fbe31fe52..11786cbdc 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -83,13 +83,20 @@ type pa_mark= Fmark of pa_fun | Cmark of pa_constructor -module PacMap=Map.Make(struct - type t=pa_constructor - let compare=Pervasives.compare end) +module PacOrd = +struct + type t = pa_constructor + let compare = Pervasives.compare (** FIXME *) +end + +module PafOrd = +struct + type t = pa_fun + let compare = Pervasives.compare (** FIXME *) +end -module PafMap=Map.Make(struct - type t=pa_fun - let compare=Pervasives.compare end) +module PacMap=Map.Make(PacOrd) +module PafMap=Map.Make(PafOrd) type cinfo= {ci_constr: constructor; (* inductive type *) diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 1b9afb7c7..75005f1c8 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -62,7 +62,8 @@ type form= | Conjunct of form * form | Disjunct of form * form -module Fmap=Map.Make(struct type t=form let compare=compare end) +module FOrd = struct type t = form let compare = Pervasives.compare (** FIXME *) end +module Fmap = Map.Make(FOrd) type sequent = {rev_hyps: form Int.Map.t; diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index f618c54b0..9614d74e2 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -332,7 +332,7 @@ type ring_info = ring_pre_tac : glob_tactic_expr; ring_post_tac : glob_tactic_expr } -module Cmap = Map.Make(struct type t = constr let compare = constr_ord end) +module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" let from_relation = Summary.ref Cmap.empty ~name:"ring-tac-rel-table" |