diff options
| author | herbelin | 2004-03-01 15:16:33 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-01 15:16:33 +0000 |
| commit | 0b4fe8fcbc69fe4564e83acba6abb4656b686db4 (patch) | |
| tree | e1bf8193c35a9bd16752c086290edc8fdbdc1095 | |
| parent | 9bfe45ef4974157c18ef18876b7df8adfb286414 (diff) | |
Ajout IntroPattern comme type d'argument générique
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5407 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/interface/xlate.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 64b5539f17..f5507e722d 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1232,6 +1232,8 @@ and coerce_genarg_to_TARG x = CT_coerce_FORMULA_OR_INT_to_TARG (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT (CT_coerce_ID_to_ID_OR_INT id)) + | IntroPatternArgType -> + xlate_error "TODO" | IdentArgType -> let id = xlate_ident (out_gen rawwit_ident x) in CT_coerce_FORMULA_OR_INT_to_TARG @@ -1322,6 +1324,8 @@ let coerce_genarg_to_VARG x = CT_coerce_ID_OPT_OR_ALL_to_VARG (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL (CT_coerce_ID_to_ID_OPT id)) + | IntroPatternArgType -> + xlate_error "TODO" | IdentArgType -> let id = xlate_ident (out_gen rawwit_ident x) in CT_coerce_ID_OPT_OR_ALL_to_VARG |