diff options
author | 2012-01-12 16:04:54 +0100 | |
---|---|---|
committer | 2012-01-12 16:04:54 +0100 | |
commit | 39efc41237ec906226a3a53d7396d51173495204 (patch) | |
tree | 87cd58d72d43469d2a2a0a127c1060d7c9e0206b /plugins/syntax/ascii_syntax.ml | |
parent | 5fe4ac437bed43547b3695664974f492b55cb553 (diff) | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'plugins/syntax/ascii_syntax.ml')
-rw-r--r-- | plugins/syntax/ascii_syntax.ml | 16 |
1 files changed, 7 insertions, 9 deletions
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) |