diff options
| -rw-r--r-- | toplevel/metasyntax.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e32e158250..1f9a08d980 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -42,7 +42,8 @@ let constr_parser_with_glob = Pcoq.map_entry constr_to_ast Constr.constr let globalize_ref vars ref = match Constrintern.interp_reference (vars,[]) ref with - | RRef (loc,a) -> Constrextern.extern_reference loc Idset.empty a + | RRef (loc,VarRef a) -> Ident (loc,a) + | RRef (loc,a) -> Qualid (loc,qualid_of_sp (Nametab.sp_of_global a)) | RVar (loc,x) -> Ident (loc,x) | _ -> anomaly "globalize_ref: not a reference" |