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

---
 plugins/syntax/ascii_syntax.ml | 47 ++++++++++++++++++++++++------------------
 1 file changed, 27 insertions(+), 20 deletions(-)

(limited to 'plugins/syntax/ascii_syntax.ml')

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index e18d19ce..acb297dd 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -1,10 +1,13 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
+(************************************************************************)
+(*         *   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          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
 
 (* Poor's man DECLARE PLUGIN *)
 let __coq_plugin_name = "ascii_syntax_plugin"
@@ -24,6 +27,10 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> Globnames.eq_gr r gr
+| _ -> false
+
 let ascii_module = ["Coq";"Strings";"Ascii"]
 
 let ascii_path = make_path ascii_module "ascii"
@@ -37,34 +44,34 @@ let glob_Ascii = lazy (make_reference "Ascii")
 
 open Lazy
 
-let interp_ascii dloc p =
+let interp_ascii ?loc p =
   let rec aux n p =
      if Int.equal n 0 then [] else
      let mp = p mod 2 in
-     GRef (dloc,(if Int.equal mp 0 then glob_false else glob_true),None)
+     (DAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None))
      :: (aux (n-1) (p/2)) in
-  GApp (dloc,GRef(dloc,force glob_Ascii,None), aux 8 p)
+  DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p)
 
-let interp_ascii_string dloc s =
+let interp_ascii_string ?loc s =
   let p =
     if Int.equal (String.length s) 1 then int_of_char s.[0]
     else
       if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
       then int_of_string s
       else
-	user_err_loc (dloc,"interp_ascii_string",
-	  str "Expects a single character or a three-digits ascii code.") in
-  interp_ascii dloc p
+	user_err ?loc ~hdr:"interp_ascii_string"
+	 (str "Expects a single character or a three-digits ascii code.") in
+  interp_ascii ?loc p
 
 let uninterp_ascii r =
   let rec uninterp_bool_list n = function
     | [] when Int.equal n 0 -> 0
-    | GRef (_,k,_)::l when Globnames.eq_gr k glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
-    | GRef (_,k,_)::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l)
+    | r::l when is_gr r glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
+    | r::l when is_gr r glob_false -> 2*(uninterp_bool_list (n-1) l)
     | _ -> raise Non_closed_ascii in
   try
-    let aux = function
-    | GApp (_,GRef (_,k,_),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l
+    let aux c = match DAst.get c with
+    | GApp (r, l) when is_gr r (force glob_Ascii) -> uninterp_bool_list 8 l
     | _ -> raise Non_closed_ascii in
     Some (aux r)
   with
@@ -74,10 +81,10 @@ let make_ascii_string n =
   if n>=32 && n<=126 then String.make 1 (char_of_int n)
   else Printf.sprintf "%03d" n
 
-let uninterp_ascii_string r = Option.map make_ascii_string (uninterp_ascii r)
+let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r)
 
 let _ =
   Notation.declare_string_interpreter "char_scope"
     (ascii_path,ascii_module)
     interp_ascii_string
-    ([GRef (Loc.ghost,static_glob_Ascii,None)], uninterp_ascii_string, true)
+    ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true)
-- 
cgit v1.2.3