diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-17 14:23:53 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 23:58:23 +0200 |
| commit | 158f40db9482ead89befbf9bc9ad45ff8a60b75f (patch) | |
| tree | 92587db07ddf50e2db16b270966115fa3d66d64a /plugins/syntax/ascii_syntax.ml | |
| parent | be83b52cf50ed4c596e40cfd52da03258a7a4a18 (diff) | |
[location] Switch glob_constr to Loc.located
Diffstat (limited to 'plugins/syntax/ascii_syntax.ml')
| -rw-r--r-- | plugins/syntax/ascii_syntax.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index ed8cc6ab0..dc0b87793 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -37,13 +37,13 @@ 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) + (Loc.tag ~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) + Loc.tag ~loc @@ GApp (Loc.tag ~loc @@ GRef(force glob_Ascii,None), aux 8 p) let interp_ascii_string dloc s = let p = @@ -59,12 +59,12 @@ let interp_ascii_string dloc s = 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) + | (_, 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) | _ -> 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 + | _, GApp ((_, GRef (k,_)),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l | _ -> raise Non_closed_ascii in Some (aux r) with @@ -80,4 +80,4 @@ 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) + ([Loc.tag @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) |