diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 6 | ||||
| -rw-r--r-- | interp/constrintern.mli | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 81ebf6561..190369e8f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -98,16 +98,16 @@ let global_reference_of_reference ref = locate_reference (snd (qualid_of_reference ref)) let global_reference id = - Universes.constr_of_global (locate_reference (qualid_of_ident id)) + locate_reference (qualid_of_ident id) let construct_reference ctx id = try - Term.mkVar (let _ = Context.Named.lookup id ctx in id) + VarRef (let _ = Context.Named.lookup id ctx in id) with Not_found -> global_reference id let global_reference_in_absolute_module dir id = - Universes.constr_of_global (Nametab.global_of_path (Libnames.make_path dir id)) + Nametab.global_of_path (Libnames.make_path dir id) (**********************************************************************) (* Internalization errors *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 644cafe57..644f60d85 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -176,9 +176,9 @@ val interp_context_evars : val locate_reference : Libnames.qualid -> Globnames.global_reference val is_global : Id.t -> bool -val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> constr -val global_reference : Id.t -> constr -val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr +val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> Globnames.global_reference +val global_reference : Id.t -> Globnames.global_reference +val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_reference (** Interprets a term as the left-hand side of a notation. The returned map is guaranteed to have the same domain as the input one. *) |