aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/reserve.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/reserve.ml')
-rw-r--r--interp/reserve.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 6fd1d0b58..22c5a2f5e 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -102,7 +102,7 @@ let declare_reserved_type idl t =
let find_reserved_type id = Id.Map.find (root_of_id id) !reserve_table
let constr_key c =
- try RefKey (canonical_gr (global_of_constr (fst (Term.decompose_app c))))
+ try RefKey (canonical_gr (global_of_constr (fst (Constr.decompose_app c))))
with Not_found -> Oth
let revert_reserved_type t =