diff options
| author | Emilio Jesus Gallego Arias | 2019-11-21 15:38:39 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-21 15:38:39 +0100 |
| commit | d016f69818b30b75d186fb14f440b93b0518fc66 (patch) | |
| tree | 32cd948273f79a2c01ad27b4ed0244ea60d7e2f9 /checker/check.ml | |
| parent | b680b06b31c27751a7d551d95839aea38f7fbea1 (diff) | |
[coq] Untabify the whole ML codebase.
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
Diffstat (limited to 'checker/check.ml')
| -rw-r--r-- | checker/check.ml | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/checker/check.ml b/checker/check.ml index 09ecd675f7..ffb2928d55 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -155,24 +155,24 @@ let add_load_path (phys_path,coq_path) = let physical, logical = !load_paths in match List.filter2 (fun p d -> p = phys_path) physical logical with | _,[dir] -> - if coq_path <> dir + if coq_path <> dir (* If this is not the default -I . to coqtop *) && not (phys_path = CUnix.canonical_path_name Filename.current_dir_name - && coq_path = default_root_prefix) - then - begin + && coq_path = default_root_prefix) + then + begin (* Assume the user is concerned by library naming *) - if dir <> default_root_prefix then - Feedback.msg_warning - (str phys_path ++ strbrk " was previously bound to " ++ - pr_dirpath dir ++ strbrk "; it is remapped to " ++ - pr_dirpath coq_path); - remove_load_path phys_path; - load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths) - end + if dir <> default_root_prefix then + Feedback.msg_warning + (str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath dir ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path); + remove_load_path phys_path; + load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths) + end | _,[] -> - load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths) + load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths) | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path^".")) let load_paths_of_dir_path dir = |