diff options
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 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)) diff --git a/interp/coqlib.ml b/interp/coqlib.ml index fa939d0aab..3a0a5047bf 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 " ")) ++ |