From d1c57fb01e6e4453520a46710455c0612656925f Mon Sep 17 00:00:00 2001
From: bertot
Date: Mon, 15 Mar 2004 13:47:01 +0000
Subject: 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
---
 contrib/interface/xlate.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3