From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 interp/reserve.ml | 28 ++++++++++++++++------------
 1 file changed, 16 insertions(+), 12 deletions(-)

(limited to 'interp/reserve.ml')

diff --git a/interp/reserve.ml b/interp/reserve.ml
index 388ca080..36005121 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Reserved names *)
@@ -71,7 +73,7 @@ let reserve_revtable = Summary.ref KeyMap.empty ~name:"reserved-type-rev"
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
   | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
   | NList (_,_,NApp (NRef ref,args),_,_)
-  | NBinderList (_,_,NApp (NRef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args)
+  | NBinderList (_,_,NApp (NRef ref,args),_,_) -> RefKey (canonical_gr ref), Some (List.length args)
   | NRef ref -> RefKey(canonical_gr ref), None
   | _ -> Oth, None
 
@@ -84,15 +86,15 @@ let in_reserved : Id.t * notation_constr -> obj =
   declare_object {(default_object "RESERVED-TYPE") with
     cache_function = cache_reserved_type }
 
-let declare_reserved_type_binding (loc,id) t =
+let declare_reserved_type_binding {CAst.loc;v=id} t =
   if not (Id.equal id (root_of_id id)) then
-    user_err_loc(loc,"declare_reserved_type",
-    (pr_id id ++ str
+    user_err ?loc ~hdr:"declare_reserved_type"
+      ((Id.print id ++ str
       " is not reservable: it must have no trailing digits, quote, or _"));
   begin try
     let _ = Id.Map.find id !reserve_table in
-    user_err_loc(loc,"declare_reserved_type",
-    (pr_id id++str" is already bound to a type"))
+    user_err ?loc ~hdr:"declare_reserved_type"
+    ((Id.print id++str" is already bound to a type"))
   with Not_found -> () end;
   add_anonymous_leaf (in_reserved (id,t))
 
@@ -102,13 +104,15 @@ 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 =
   try
+    let t = EConstr.Unsafe.to_constr t in
     let reserved = KeyMap.find (constr_key t) !reserve_revtable in
-    let t = Detyping.detype false [] (Global.env()) Evd.empty t in
+    let t = EConstr.of_constr t in
+    let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in
     (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
         then I've introduced a bug... *)
     let filter _ pat =
-- 
cgit v1.2.3