diff options
Diffstat (limited to 'parsing/esyntax.ml')
| -rw-r--r-- | parsing/esyntax.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml index 608868ca6a..b3d0278028 100644 --- a/parsing/esyntax.ml +++ b/parsing/esyntax.ml @@ -10,6 +10,8 @@ open Pp open Util +open Names +open Libnames open Coqast open Ast open Extend @@ -195,14 +197,14 @@ let make_hunks (lp,rp) s e1 e2 = let build_syntax (ref,e1,e2,assoc) = let sp = match ref with - | TrueGlobal r -> Nametab.sp_of_global (Global.env()) r - | SyntacticDef sp -> sp in + | TrueGlobal r -> Nametab.sp_of_global None r + | SyntacticDef kn -> Nametab.sp_of_syntactic_definition kn in let rec find_symbol = function | [] -> let s = match ref with | TrueGlobal r -> - string_of_qualid (shortest_qualid_of_global (Global.env()) r) - | SyntacticDef sp -> string_of_path sp in + string_of_qualid (shortest_qualid_of_global None r) + | SyntacticDef _ -> string_of_path sp in UNP_BOX (PpHOVB 0, [RO "("; RO s; UNP_BRK (1, 1); PH (meta_pattern e1, None, E); UNP_BRK (1, 1); PH (meta_pattern e2, None, E); RO ")"]) |