aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.ml
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-28 09:24:15 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-28 09:24:15 +0000
commitf7665a72dba3a896997220d738597cfe05b27990 (patch)
tree9bf47da71e2a912832199c6d13633d8ddee34678 /toplevel/metasyntax.ml
parent059a0622a512e40ffc1944cdc6084c3462aa85f9 (diff)
Fixes in generalize_eqs/dependent induction to allow the user to specify
generalized variables himself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11280 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/metasyntax.ml')
0 files changed, 0 insertions, 0 deletions