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 | |
| 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
| -rw-r--r-- | contrib/interface/xlate.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index fad049a06b..a388605ad3 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -308,7 +308,7 @@ and xlate_return_info = function CT_coerce_NONE_to_RETURN_INFO CT_none | (None, Some t) -> CT_return(xlate_formula t) | (Some x, Some t) -> CT_as_and_return(xlate_id_opt_aux x, xlate_formula t) - +| (Some Anonymous, None) -> CT_coerce_NONE_to_RETURN_INFO CT_none | (Some _, None) -> assert false and xlate_formula_opt = function |