aboutsummaryrefslogtreecommitdiff
path: root/doc/tutorial
diff options
context:
space:
mode:
authorletouzey2010-02-13 14:37:11 +0000
committerletouzey2010-02-13 14:37:11 +0000
commit2b73159ba68c43c881b6c8a64134cbc473c9dc91 (patch)
treecb3bbd26c1fc7a930118aa5ad8152c5a4caec6ca /doc/tutorial
parentb66f8bf69668b503eba9b815a588b722f8aeadc5 (diff)
Fix NumbersSyntax.out
Having to alias the inductive BigN.t_ by a constant BigN.t for satisfying the NSig interface is just a pain. Let's hope it could change someday. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12763 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/tutorial')
0 files changed, 0 insertions, 0 deletions