diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-19 16:16:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-19 16:16:43 +0000 |
| commit | 7008fddba4b0a1ac9e46c0bf5af8ea09839232c8 (patch) | |
| tree | 2d0056ca3dd845a5aa7377ef60cc8e9e9cdf0956 | |
| parent | cddb721edc8c2e61b29a64349cd199c0dfce3d11 (diff) | |
Suite 11472
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11473 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/interface/xlate.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 8c470f1bd..77cde062f 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1304,11 +1304,13 @@ and coerce_genarg_to_TARG x = (CT_coerce_ID_to_ID_OR_INT id)) | IntroPatternArgType -> xlate_error "TODO" - | IdentArgType -> + | IdentArgType true -> let id = xlate_ident (out_gen rawwit_ident x) in CT_coerce_FORMULA_OR_INT_to_TARG (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT (CT_coerce_ID_to_ID_OR_INT id)) + | IdentArgType false -> + xlate_error "TODO" | VarArgType -> let id = xlate_ident (snd (out_gen rawwit_var x)) in CT_coerce_FORMULA_OR_INT_to_TARG @@ -1402,11 +1404,13 @@ let coerce_genarg_to_VARG x = (CT_coerce_ID_to_ID_OPT id)) | IntroPatternArgType -> xlate_error "TODO" - | IdentArgType -> + | IdentArgType true -> let id = xlate_ident (out_gen rawwit_ident x) in CT_coerce_ID_OPT_OR_ALL_to_VARG (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL (CT_coerce_ID_to_ID_OPT id)) + | IdentArgType false -> + xlate_error "TODO" | VarArgType -> let id = xlate_ident (snd (out_gen rawwit_var x)) in CT_coerce_ID_OPT_OR_ALL_to_VARG |