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

---
 parsing/g_prim.ml4 | 53 ++++++++++++++++++++++++++++-------------------------
 1 file changed, 28 insertions(+), 25 deletions(-)

(limited to 'parsing/g_prim.ml4')

diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index b90e06cd..b25ea766 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -1,15 +1,15 @@
 (************************************************************************)
-(*  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)         *)
 (************************************************************************)
 
-open Compat
 open Names
 open Libnames
-open Tok (* necessary for camlp4 *)
 
 open Pcoq
 open Pcoq.Prim
@@ -28,13 +28,13 @@ let my_int_of_string loc s =
     if n > 1024 * 2048 then raise Exit;
     n
   with Failure _ | Exit ->
-    CErrors.user_err_loc (loc,"",Pp.str "Cannot support a so large number.")
+    CErrors.user_err ~loc  (Pp.str "Cannot support a so large number.")
 
 GEXTEND Gram
   GLOBAL:
     bigint natural integer identref name ident var preident
     fullyqualid qualid reference dirpath ne_lstring
-    ne_string string pattern_ident pattern_identref by_notation smart_global;
+    ne_string string lstring pattern_ident pattern_identref by_notation smart_global;
   preident:
     [ [ s = IDENT -> s ] ]
   ;
@@ -45,13 +45,13 @@ GEXTEND Gram
     [ [ LEFTQMARK; id = ident -> id ] ]
   ;
   pattern_identref:
-    [ [ id = pattern_ident -> (!@loc, id) ] ]
+    [ [ id = pattern_ident -> CAst.make ~loc:!@loc id ] ]
   ;
   var: (* as identref, but interpret as a term identifier in ltac *)
-    [ [ id = ident -> (!@loc, id) ] ]
+    [ [ id = ident -> CAst.make ~loc:!@loc id ] ]
   ;
   identref:
-    [ [ id = ident -> (!@loc, id) ] ]
+    [ [ id = ident -> CAst.make ~loc:!@loc id ] ]
   ;
   field:
     [ [ s = FIELD -> Id.of_string s ] ]
@@ -62,8 +62,8 @@ GEXTEND Gram
       ] ]
   ;
   fullyqualid:
-    [ [ id = ident; (l,id')=fields -> !@loc,id::List.rev (id'::l)
-      | id = ident -> !@loc,[id]
+    [ [ id = ident; (l,id')=fields -> CAst.make ~loc:!@loc @@ id::List.rev (id'::l)
+      | id = ident -> CAst.make ~loc:!@loc [id]
       ] ]
   ;
   basequalid:
@@ -72,32 +72,32 @@ GEXTEND Gram
       ] ]
   ;
   name:
-    [ [ IDENT "_" -> (!@loc, Anonymous)
-      | id = ident -> (!@loc, Name id) ] ]
+    [ [ IDENT "_"  -> CAst.make ~loc:!@loc Anonymous
+      | id = ident -> CAst.make ~loc:!@loc @@ Name id ] ]
   ;
   reference:
     [ [ id = ident; (l,id') = fields ->
-        Qualid (!@loc, local_make_qualid (l@[id]) id')
-      | id = ident -> Ident (!@loc,id)
+        CAst.make ~loc:!@loc @@ Qualid (local_make_qualid (l@[id]) id')
+      | id = ident -> CAst.make ~loc:!@loc @@ Ident id
       ] ]
   ;
   by_notation:
-    [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (!@loc, s, sc) ] ]
+    [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (s, sc) ] ]
   ;
   smart_global:
-    [ [ c = reference -> Misctypes.AN c
-      | ntn = by_notation -> Misctypes.ByNotation ntn ] ]
+    [ [ c = reference -> CAst.make ~loc:!@loc @@ Misctypes.AN c
+      | ntn = by_notation -> CAst.make ~loc:!@loc @@ Misctypes.ByNotation ntn ] ]
   ;
   qualid:
-    [ [ qid = basequalid -> !@loc, qid ] ]
+    [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ]
   ;
   ne_string:
     [ [ s = STRING ->
-        if s="" then CErrors.user_err_loc(!@loc, "", Pp.str"Empty string."); s
+        if s="" then CErrors.user_err ~loc:!@loc (Pp.str"Empty string."); s
     ] ]
   ;
   ne_lstring:
-    [ [ s = ne_string -> (!@loc, s) ] ]
+    [ [ s = ne_string -> CAst.make ~loc:!@loc s ] ]
   ;
   dirpath:
     [ [ id = ident; l = LIST0 field ->
@@ -106,6 +106,9 @@ GEXTEND Gram
   string:
     [ [ s = STRING -> s ] ]
   ;
+  lstring:
+    [ [ s = string -> (CAst.make ~loc:!@loc s) ] ]
+  ;
   integer:
     [ [ i = INT      -> my_int_of_string (!@loc) i
       | "-"; i = INT -> - my_int_of_string (!@loc) i ] ]
@@ -113,7 +116,7 @@ GEXTEND Gram
   natural:
     [ [ i = INT -> my_int_of_string (!@loc) i ] ]
   ;
-  bigint: (* Negative numbers are dealt with specially *)
-    [ [ i = INT -> (Bigint.of_string i) ] ]
+  bigint: (* Negative numbers are dealt with elsewhere *)
+    [ [ i = INT -> i ] ]
   ;
 END
-- 
cgit v1.2.3