aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/g_extraction.ml4
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-05 16:42:46 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-05 16:42:46 +0000
commit8c376b71eb6ebc72ec44fd980dc282b8796299c7 (patch)
tree4a58bbc01bfbbf8dacb4ff58d68afa0cd3921244 /plugins/extraction/g_extraction.ml4
parent19d89158f4e0e4be5998f2ff9b64e90270977a32 (diff)
Added a table for using reserved names for binding names to types
(in addition of types to names) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13887 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/g_extraction.ml4')
0 files changed, 0 insertions, 0 deletions