diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /plugins/syntax/ascii_syntax.ml | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax/ascii_syntax.ml')
| -rw-r--r-- | plugins/syntax/ascii_syntax.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index f9ca94ff6..f60abaf85 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -38,7 +38,7 @@ let glob_Ascii = lazy (make_reference "Ascii") open Lazy let interp_ascii dloc p = - let rec aux n 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) @@ -46,7 +46,7 @@ let interp_ascii dloc p = RApp (dloc,RRef(dloc,force glob_Ascii), aux 8 p) let interp_ascii_string dloc s = - let p = + let p = if String.length s = 1 then int_of_char s.[0] else if String.length s = 3 & is_digit s.[0] & is_digit s.[1] & is_digit s.[2] @@ -62,12 +62,12 @@ let uninterp_ascii r = | 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) | _ -> raise Non_closed_ascii in - try + try let rec aux = function | RApp (_,RRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l | _ -> raise Non_closed_ascii in Some (aux r) - with + with Non_closed_ascii -> None let make_ascii_string n = |