aboutsummaryrefslogtreecommitdiff
path: root/interp/syntax_def.ml
diff options
context:
space:
mode:
authorherbelin2003-04-11 08:54:07 +0000
committerherbelin2003-04-11 08:54:07 +0000
commita04706bd19e8ebc06fdb9c9f7eebd049edd4a9f3 (patch)
treec4c9e6bd136d08b0ad766a2d1aa73e2ac5bbe534 /interp/syntax_def.ml
parent373091ffbab347d8b75831e17f3e4384018facd8 (diff)
Explicitation arguments de eq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3914 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/syntax_def.ml')
0 files changed, 0 insertions, 0 deletions