diff options
| author | Matthieu Sozeau | 2017-05-29 11:48:51 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2017-05-29 11:58:48 +0200 |
| commit | fd7f056b155b2ebaafa3251a3c136117ebefc3e3 (patch) | |
| tree | 46ff14eb398806485d148757a2f34e1889ef7aaf /interp | |
| parent | 4c1260299b707bd27765b0ab365092046b134a69 (diff) | |
Cleanup: removal of constr_of_global.
Constrintern.pf_global returns a global_reference, not a constr,
adapt plugins accordingly, properly registering universes where
necessary.
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 4dcf287efc..628c85e755 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 644cafe575..644f60d850 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. *) |