diff options
| author | Maxime Dénès | 2018-09-13 18:07:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-13 18:07:55 +0200 |
| commit | 8500216ac8df90b2afc0f5fd42d714cc87c6bde6 (patch) | |
| tree | 76a1ebe10646d2432f1539fb7ee9c6b0691ea221 /pretyping/reductionops.ml | |
| parent | 9281bb33f2b9aa5d762f8b5b8b0159984b696efb (diff) | |
| parent | 8fafc201699e3d6c80e39bbadf2e6a5ba6425036 (diff) | |
Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernel
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f133eb9963..f4c8a6cd66 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -88,6 +88,7 @@ let set_reduction_effect x funkey = (** Machinery to custom the behavior of the reduction *) module ReductionBehaviour = struct open Globnames + open Names open Libobject type t = { @@ -97,7 +98,7 @@ module ReductionBehaviour = struct } let table = - Summary.ref (Refmap.empty : t Refmap.t) ~name:"reductionbehaviour" + Summary.ref (GlobRef.Map.empty : t GlobRef.Map.t) ~name:"reductionbehaviour" type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ] type req = @@ -105,7 +106,7 @@ module ReductionBehaviour = struct | ReqGlobal of GlobRef.t * (int list * int * flag list) let load _ (_,(_,(r, b))) = - table := Refmap.add r b !table + table := GlobRef.Map.add r b !table let cache o = load 1 o @@ -160,7 +161,7 @@ module ReductionBehaviour = struct let get r = try - let b = Refmap.find r !table in + let b = GlobRef.Map.find r !table in let flags = if Int.equal b.b_nargs max_int then [`ReductionNeverUnfold] else if b.b_dont_expose_case then [`ReductionDontExposeCase] else [] in |