fact: Definition mod_rewrite (t : string) (mds : mod_data) : option string := let (ds,d) := mds in match rewrites E t ds with | None => None | Some ts => rewrite R (last ts t) d end.
imports: Coq(Euclid Wf_nat) CoLoR(Srs LogicUtil SLoop ListUtil NatUtil RelUtil)