aboutsummaryrefslogtreecommitdiff
path: root/pretyping/glob_ops.mli
AgeCommit message (Expand)Author
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:30:38 +0000