diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-11-28 20:23:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-11-29 10:56:36 +0100 |
| commit | 45192ccb907349f0ec51c3d2ac577920c4016119 (patch) | |
| tree | dcda1c5bd25c2d1946cfbc9672a2d6a457659188 /checker/checker.ml | |
| parent | 0168f040e29c3bbaeb666f0b793f41627f154e12 (diff) | |
Allow to pass physical files to coqchk.
Diffstat (limited to 'checker/checker.ml')
| -rw-r--r-- | checker/checker.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index e960a55fd..b2433ee36 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -40,9 +40,10 @@ let dirpath_of_string s = [] -> Check.default_root_prefix | dir -> DirPath.make (List.map Id.of_string dir) let path_of_string s = - match parse_dir s with + if Filename.check_suffix s ".vo" then PhysicalFile s + else match parse_dir s with [] -> invalid_arg "path_of_string" - | l::dir -> {dirpath=dir; basename=l} + | l::dir -> LogicalFile {dirpath=dir; basename=l} let ( / ) = Filename.concat @@ -144,15 +145,15 @@ let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet let engage () = Safe_typing.set_engagement (!impredicative_set) -let admit_list = ref ([] : section_path list) +let admit_list = ref ([] : object_file list) let add_admit s = admit_list := path_of_string s :: !admit_list -let norec_list = ref ([] : section_path list) +let norec_list = ref ([] : object_file list) let add_norec s = norec_list := path_of_string s :: !norec_list -let compile_list = ref ([] : section_path list) +let compile_list = ref ([] : object_file list) let add_compile s = compile_list := path_of_string s :: !compile_list |