diff options
| author | herbelin | 2009-11-11 16:03:06 +0000 |
|---|---|---|
| committer | herbelin | 2009-11-11 16:03:06 +0000 |
| commit | e46a343090514c1340d4e5b97384b55b42c9c166 (patch) | |
| tree | afe12355bdb7e823b5881b4a89d54b6753684001 /plugins/interface/xlate.ml | |
| parent | d27a272511939ba80f1b3658be064268ec9ba55e (diff) | |
Added support for multiple where-clauses in Inductive and co (see wish #2163).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12500 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface/xlate.ml')
| -rw-r--r-- | plugins/interface/xlate.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index 435130ae6f..7b35f4021b 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -1555,13 +1555,14 @@ let xlate_comment = function (CT_coerce_NUM_to_FORMULA(CT_int_encapsulator (string_of_int n)));; let translate_opt_notation_decl = function - None -> CT_coerce_NONE_to_DECL_NOTATION_OPT(CT_none) - | Some(s, f, sc) -> + [] -> CT_coerce_NONE_to_DECL_NOTATION_OPT(CT_none) + | [s, f, sc] -> let tr_sc = match sc with None -> ctv_ID_OPT_NONE | Some id -> CT_coerce_ID_to_ID_OPT (CT_ident id) in - CT_decl_notation(CT_string s, xlate_formula f, tr_sc);; + CT_decl_notation(CT_string s, xlate_formula f, tr_sc) + | _ -> xlate_error "TODO: multiple where clause";; let xlate_level = function Extend.NumLevel n -> CT_coerce_INT_to_INT_OR_NEXT(CT_int n) |