aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/find_subterm.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-18 21:21:01 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-18 21:21:01 +0200
commita7e66e4f3af85be7a4d345d0f8c6bde5a7a0c7b0 (patch)
treec03ee45c7e0f7b6ed7bfd21c52b9e3295684490b /pretyping/find_subterm.ml
parent892c74d099fd9eda1e2f179645f7e1d9b67ba49b (diff)
Clean a bit of univ.ml, add credits.
Diffstat (limited to 'pretyping/find_subterm.ml')
0 files changed, 0 insertions, 0 deletions