diff options
| author | bertot | 2004-03-15 13:47:01 +0000 |
|---|---|---|
| committer | bertot | 2004-03-15 13:47:01 +0000 |
| commit | d1c57fb01e6e4453520a46710455c0612656925f (patch) | |
| tree | 5823888a8928d65ca3d04b443137ce0c6284d0d1 /dev/base_include | |
| parent | f1867d585ca054e038e26c3dc2eaf8350d918b5b (diff) | |
To make that the translation process does not fail on data produced by
the logical engine (rather than the parser), where Some Anonymous appears instead
of None in the patterns of xlate_return_info
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5486 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions