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/smartlocate.ml | 56 +++++++++++++++++++++++++--------------------------
 1 file changed, 27 insertions(+), 29 deletions(-)

(limited to 'interp/smartlocate.ml')

diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 47877421..1f4a93a6 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.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)         *)
 (************************************************************************)
 
 (* Created by Hugo Herbelin from code formerly dispatched in
@@ -28,7 +30,7 @@ let global_of_extended_global_head = function
         | NRef ref -> ref
         | NApp (rc, _) -> head_of rc
         | NCast (rc, _) -> head_of rc
-        | NLetIn (_, _, rc) -> head_of rc
+        | NLetIn (_, _, _, rc) -> head_of rc
         | _ -> raise Not_found in
       head_of syn_def
 
@@ -40,42 +42,38 @@ let global_of_extended_global = function
   | [],NApp (NRef ref,[]) -> ref
   | _ -> raise Not_found
 
-let locate_global_with_alias ?(head=false) (loc,qid) =
+let locate_global_with_alias ?(head=false) {CAst.loc; v=qid} =
   let ref = Nametab.locate_extended qid in
   try
     if head then global_of_extended_global_head ref
     else global_of_extended_global ref
   with Not_found ->
-    user_err_loc (loc,"",pr_qualid qid ++
+    user_err ?loc (pr_qualid qid ++
       str " is bound to a notation that does not denote a reference.")
 
-let global_inductive_with_alias r =
-  let (loc,qid as lqid) = qualid_of_reference r in
-  try match locate_global_with_alias lqid with
+let global_inductive_with_alias ({CAst.loc} as lr)  =
+  let qid = qualid_of_reference lr in
+  try match locate_global_with_alias qid with
   | IndRef ind -> ind
   | ref ->
-      user_err_loc (loc_of_reference r,"global_inductive",
-        pr_reference r ++ spc () ++ str "is not an inductive type.")
-  with Not_found -> Nametab.error_global_not_found_loc loc qid
+      user_err ?loc ~hdr:"global_inductive"
+        (pr_reference lr ++ spc () ++ str "is not an inductive type.")
+  with Not_found -> Nametab.error_global_not_found qid
 
 let global_with_alias ?head r =
-  let (loc,qid as lqid) = qualid_of_reference r in
-  try locate_global_with_alias ?head lqid
-  with Not_found -> Nametab.error_global_not_found_loc loc qid
+  let qid = qualid_of_reference r in
+  try locate_global_with_alias ?head qid
+  with Not_found -> Nametab.error_global_not_found qid
 
-let smart_global ?head = function
+let smart_global ?head = CAst.with_loc_val (fun ?loc -> function
   | AN r ->
-      global_with_alias ?head r
-  | ByNotation (loc,ntn,sc) ->
-      Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc
+    global_with_alias ?head r
+  | ByNotation (ntn,sc) ->
+    Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)
 
-let smart_global_inductive = function
+let smart_global_inductive = CAst.with_loc_val (fun ?loc -> function
   | AN r ->
-      global_inductive_with_alias r
-  | ByNotation (loc,ntn,sc) ->
-      destIndRef
-        (Notation.interp_notation_as_global_reference loc isIndRef ntn sc)
-
-let loc_of_smart_reference = function
-  | AN r -> loc_of_reference r
-  | ByNotation (loc,_,_) -> loc
+    global_inductive_with_alias r
+  | ByNotation (ntn,sc) ->
+    destIndRef
+      (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc))
-- 
cgit v1.2.3