From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 plugins/syntax/ascii_syntax.ml | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

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

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index ae3afff4..bd2285bb 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -6,13 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id: ascii_syntax.ml 12406 2009-10-21 15:12:52Z soubiran $ i*)
-
 open Pp
 open Util
 open Names
 open Pcoq
-open Rawterm
+open Glob_term
 open Topconstr
 open Libnames
 open Coqlib
@@ -41,9 +39,9 @@ let interp_ascii dloc p =
   let rec aux n p =
      if n = 0 then [] else
      let mp = p mod 2 in
-     RRef (dloc,if mp = 0 then glob_false else glob_true)
+     GRef (dloc,if mp = 0 then glob_false else glob_true)
      :: (aux (n-1) (p/2)) in
-  RApp (dloc,RRef(dloc,force glob_Ascii), aux 8 p)
+  GApp (dloc,GRef(dloc,force glob_Ascii), aux 8 p)
 
 let interp_ascii_string dloc s =
   let p =
@@ -59,12 +57,12 @@ let interp_ascii_string dloc s =
 let uninterp_ascii r =
   let rec uninterp_bool_list n = function
     | [] when n = 0 -> 0
-    | RRef (_,k)::l when k = glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
-    | RRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l)
+    | GRef (_,k)::l when k = glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
+    | GRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l)
     | _ -> raise Non_closed_ascii in
   try
     let rec aux = function
-    | RApp (_,RRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l
+    | GApp (_,GRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l
     | _ -> raise Non_closed_ascii in
     Some (aux r)
   with
@@ -80,4 +78,4 @@ let _ =
   Notation.declare_string_interpreter "char_scope"
     (ascii_path,ascii_module)
     interp_ascii_string
-    ([RRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true)
+    ([GRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true)
-- 
cgit v1.2.3