diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-01-06 00:58:42 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-01-06 00:58:42 +0100 |
| commit | 23cbf43f353c50fa72b72d694611c5c14367cea2 (patch) | |
| tree | a04f140b3f383a798b3aeca9b92f663ff0d98dba /plugins | |
| parent | ffc135337b479349a9e94c0da0a87531cf0684fa (diff) | |
Protect code against changes in Map interface.
The Map interface of upcoming OCaml 4.03 includes a new union operator. In
order to make our homemade implementation of Maps compatible with OCaml
versions from 3.12 to 4.03, we define our own signatures for Maps.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/cc/ccalgo.mli | 6 | ||||
| -rw-r--r-- | plugins/extraction/table.mli | 2 | ||||
| -rw-r--r-- | plugins/firstorder/sequent.mli | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 0dcf3a870..34c19958a 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -20,8 +20,8 @@ type pa_fun= fnargs:int} -module PafMap : Map.S with type key = pa_fun -module PacMap : Map.S with type key = pa_constructor +module PafMap : CSig.MapS with type key = pa_fun +module PacMap : CSig.MapS with type key = pa_constructor type cinfo = {ci_constr: pconstructor; (* inductive type *) @@ -185,7 +185,7 @@ val empty_forest: unit -> forest (*type pa_constructor -module PacMap:Map.S with type key=pa_constructor +module PacMap:CSig.MapS with type key=pa_constructor type term = Symb of Term.constr diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 916cf3ad6..4e638a0ac 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -13,7 +13,7 @@ open Miniml open Declarations module Refset' : CSig.SetS with type elt = global_reference -module Refmap' : Map.S with type key = global_reference +module Refmap' : CSig.MapS with type key = global_reference val safe_basename_of_global : global_reference -> Id.t diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index dc3f05be6..760168c9f 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -13,7 +13,7 @@ open Globnames module OrderedConstr: Set.OrderedType with type t=constr -module CM: Map.S with type key=constr +module CM: CSig.MapS with type key=constr type h_item = global_reference * (int*constr) option |