diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/rawterm_to_relation.ml | 2 | ||||
| -rw-r--r-- | plugins/interface/name_to_ast.ml | 2 | ||||
| -rw-r--r-- | plugins/interface/xlate.ml | 7 | ||||
| -rw-r--r-- | plugins/subtac/subtac_command.ml | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac_command.mli | 4 |
7 files changed, 12 insertions, 11 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 77389681b..bd3f7e8ec 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -527,7 +527,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id)) in - (name,annot,args,types,body),(None:Vernacexpr.decl_notation option) + (name,annot,args,types,body),([]:Vernacexpr.decl_notation list) | (name,None,args,types,body),recdef -> let names = (Topconstr.names_of_local_assums args) in if is_one_rec recdef && List.length names > 1 then @@ -537,7 +537,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp else let loc, na = List.hd names in (name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body), - (None:Vernacexpr.decl_notation option) + ([]:Vernacexpr.decl_notation list) | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> error ("Cannot use mutual definition with well-founded recursion or measure") diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 04e36d945..c69e04b93 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -904,7 +904,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) } in *) let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) - let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,None)] in + let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (Command.declare_mutual_inductive_with_eliminations false mie impls) diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml index 752e546c8..f69dd2fe6 100644 --- a/plugins/funind/rawterm_to_relation.ml +++ b/plugins/funind/rawterm_to_relation.ml @@ -1338,7 +1338,7 @@ let do_build_inductive ((dummy_loc,relnames.(i)), rel_params, Some rel_arities.(i), - ext_rel_constructors),None + ext_rel_constructors),[] in let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in let rel_inds = Array.to_list ext_rel_constructors in diff --git a/plugins/interface/name_to_ast.ml b/plugins/interface/name_to_ast.ml index 142116ade..b87d95a82 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 435130ae6..7b35f4021 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) diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 007013d40..b61299a06 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -431,7 +431,7 @@ let interp_recursive fixkind l boxed = (* Get interpretation metadatas *) let impls = Constrintern.compute_full_internalization_env env Constrintern.Recursive [] fixnames fixtypes fiximps in - let notations = List.fold_right Option.List.cons ntnl [] in + let notations = List.flatten ntnl in (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli index c9064ec82..71c93266d 100644 --- a/plugins/subtac/subtac_command.mli +++ b/plugins/subtac/subtac_command.mli @@ -54,7 +54,7 @@ val build_wellfounded : Topconstr.constr_expr -> 'b -> 'c -> Subtac_obligations.progress val build_recursive : - (fixpoint_expr * decl_notation option) list -> bool -> unit + (fixpoint_expr * decl_notation list) list -> bool -> unit val build_corecursive : - (cofixpoint_expr * decl_notation option) list -> bool -> unit + (cofixpoint_expr * decl_notation list) list -> bool -> unit |