+ (* Variables used in backward compatibility code to map
+ theory:/path/t.theory into theory:/path/t/index.theory
+ when cic:/path/t/ exists *)
+ let the_candidate_for_remapping =
+ (* CSC: Here I am making a strong assumption: the pattern
+ can be only of the form [^:]*:/path where path is
+ NOT a regular expression *)
+ "theory:" ^ Pcre.replace ~rex:(Pcre.regexp "[^:]*:") pat
+ in
+ let index_not_generated_yet = ref true in
+ let valid_candidates = ref [] in
+ let candidates_found = ref [] in