diff options
| author | ppedrot | 2013-08-25 22:34:08 +0000 |
|---|---|---|
| committer | ppedrot | 2013-08-25 22:34:08 +0000 |
| commit | f4a6a6aaa928e7a6c8d360c45268cb82c020c2dc (patch) | |
| tree | 95bf369c1f34a6a4c055357b68e60de58849bd11 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/evd.mli | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index e67b1f81bd..59e176543f 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Loc open Pp open Names @@ -19,9 +20,8 @@ open Termops (******************************************************************** Meta map *) -module Metamap : Map.S with type key = metavariable - module Metaset : Set.S with type elt = metavariable +module Metamap : Map.ExtS with type key = metavariable and module Set := Metaset type 'a freelisted = { rebus : 'a; @@ -187,8 +187,10 @@ type conv_pb = Reduction.conv_pb type evar_constraint = conv_pb * env * constr * constr val add_conv_pb : evar_constraint -> evar_map -> evar_map -module ExistentialMap : Map.S with type key = existential_key module ExistentialSet : Set.S with type elt = existential_key +module ExistentialMap : Map.ExtS + with type key = existential_key and module Set := ExistentialSet + val extract_changed_conv_pbs : evar_map -> (ExistentialSet.t -> evar_constraint -> bool) -> evar_map * evar_constraint list |