diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4dcf287ef..628c85e75 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 *) |