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 | |
| 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')
| -rw-r--r-- | plugins/interface/name_to_ast.ml | 2 | ||||
| -rw-r--r-- | plugins/interface/xlate.ml | 7 |
2 files changed, 5 insertions, 4 deletions
diff --git a/plugins/interface/name_to_ast.ml b/plugins/interface/name_to_ast.ml index 142116adea..b87d95a824 100644 --- a/plugins/interface/name_to_ast.ml +++ b/plugins/interface/name_to_ast.ml @@ -110,7 +110,7 @@ let convert_one_inductive sp tyi = (((false,(dummy_loc,basename sp)), convert_env(List.rev params), Some (extern_constr true envpar arity), Vernacexpr.Inductive_kw , - Constructors (convert_constructors envpar cstrnames cstrtypes)), None);; + Constructors (convert_constructors envpar cstrnames cstrtypes)), []);; (* This function converts a Mutual inductive definition to a Coqast.t. It is obtained directly from print_mutual in pretty.ml. However, all 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) |