diff options
Diffstat (limited to 'interp/reserve.ml')
| -rw-r--r-- | interp/reserve.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml index 36005121..071248f0 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -22,7 +22,7 @@ open Notation_ops open Globnames type key = - | RefKey of global_reference + | RefKey of GlobRef.t | Oth (** TODO: share code from Notation *) @@ -112,7 +112,9 @@ let revert_reserved_type t = let t = EConstr.Unsafe.to_constr t in let reserved = KeyMap.find (constr_key t) !reserve_revtable in let t = EConstr.of_constr t in - let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in + let env = Global.env () in + let evd = Evd.from_env env in + let t = Detyping.detype Detyping.Now false Id.Set.empty env evd t in (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _] then I've introduced a bug... *) let filter _ pat = |