diff options
Diffstat (limited to 'plugins/funind/merge.ml')
| -rw-r--r-- | plugins/funind/merge.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index ea699580..e3455e77 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -841,7 +841,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = FIXME: params et cstr_expr (arity) *) let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift (rawlist:(Id.t * glob_constr) list) = - let lident = Loc.ghost, shift.ident in + let lident = (Loc.ghost, shift.ident), None in let bindlist , cstr_expr = (* params , arities *) merge_rec_params_and_arity prms1 prms2 shift mkSet in let lcstor_expr : (bool * (lident * constr_expr)) list = @@ -884,10 +884,10 @@ let merge_inductive (ind1: inductive) (ind2: inductive) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,impls = Command.interp_mutual_inductive indl [] + let mie,pl,impls = Command.interp_mutual_inductive indl [] false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) - ignore (Command.declare_mutual_inductive_with_eliminations mie impls) + ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) (* Find infos on identifier id. *) @@ -902,7 +902,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info = (** [merge id1 id2 args1 args2 id] builds and declares a new inductive type called [id], representing the merged graphs of both graphs - [ind1] and [ind2]. identifiers occuring in both arrays [args1] and + [ind1] and [ind2]. identifiers occurring in both arrays [args1] and [args2] are considered linked (i.e. are the same variable) in the new graph. |