diff options
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
| -rw-r--r-- | plugins/xml/xmlcommand.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 1ae186614..4a27c3247 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -102,7 +102,7 @@ let filter_params pvars hyps = in let cwd = Lib.cwd () in let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in - let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in + let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in aux (Names.repr_dirpath modulepath) (List.rev pvars) ;; @@ -118,7 +118,7 @@ let search_variables () = let module N = Names in let cwd = Lib.cwd () in let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in - let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in + let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in let rec aux = function [] -> [] |