aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/extend.ml
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-29 21:53:30 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-29 21:53:30 +0000
commit7cae78ffc70a9097beb6d0f1a0e9f741f483e591 (patch)
tree3908b81ac623f7910578365a4fe4b18b607de3d5 /parsing/extend.ml
parentdfe97724fb6034fc06b3ef693f6a3ed94733adbc (diff)
Exports manquants dans ring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9315 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/extend.ml')
0 files changed, 0 insertions, 0 deletions