diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-18 22:14:57 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-18 22:14:57 +0000 |
| commit | d56dbd226a805d93d539c63e9fa89062572bb295 (patch) | |
| tree | ffe757ec9a756e061b6a22270814e5417b790732 /interp | |
| 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')
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/coqlib.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index dd9ddb16d..3a9dc3a75 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)) diff --git a/interp/coqlib.ml b/interp/coqlib.ml index fa939d0aa..3a0a5047b 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -31,7 +31,7 @@ let gen_reference locstr dir s = anomaly (locstr^": cannot find "^(string_of_path sp)) let gen_constant locstr dir s = - constr_of_reference (gen_reference locstr dir s) + constr_of_global (gen_reference locstr dir s) let list_try_find f = let rec try_find_f = function @@ -50,7 +50,7 @@ let gen_constant_in_modules locstr dirs s = let all = Nametab.locate_all (make_short_qualid id) in let these = List.filter (has_suffix_in_dirs dirs) all in match these with - | [x] -> constr_of_reference x + | [x] -> constr_of_global x | [] -> anomalylabstrm "" (str (locstr^": cannot find "^s^ " in module"^(if List.length dirs > 1 then "s " else " ")) ++ |