diff options
| author | herbelin | 2005-02-18 22:14:57 +0000 |
|---|---|---|
| committer | herbelin | 2005-02-18 22:14:57 +0000 |
| commit | d56dbd226a805d93d539c63e9fa89062572bb295 (patch) | |
| tree | ffe757ec9a756e061b6a22270814e5417b790732 /interp/constrintern.ml | |
| parent | f1c9b401cf40df87eb4be7ca512a6bc199f09b7c (diff) | |
Standardisation of function names about global references (especially, renaming of constr_of_reference into constr_of_global)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6745 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index dd9ddb16da..3a9dc3a75a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1198,7 +1198,7 @@ let is_global id = false let global_reference id = - constr_of_reference (locate_reference (make_short_qualid id)) + constr_of_global (locate_reference (make_short_qualid id)) let construct_reference ctx id = try @@ -1207,5 +1207,5 @@ let construct_reference ctx id = global_reference id let global_reference_in_absolute_module dir id = - constr_of_reference (Nametab.absolute_reference (Libnames.make_path dir id)) + constr_of_global (Nametab.absolute_reference (Libnames.make_path dir id)) |