aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorlmamane2009-02-11 09:14:20 +0000
committerlmamane2009-02-11 09:14:20 +0000
commitf1f56d9f8ea26b74227bf381ce581c9aadf75c27 (patch)
tree2dabb59cd2b6e05b790be1dcf5bdbe812498ec1f /kernel/type_errors.ml
parent6afa8653207732d3cd0e9d5a2d77665369036bf0 (diff)
Convert all uses of FIND_VCS_CLAUSE to recommended style
(which allows to get rid of '-type f' hack) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11908 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions