diff options
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" |