summaryrefslogtreecommitdiff
path: root/plugins/funind/merge.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /plugins/funind/merge.ml
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'plugins/funind/merge.ml')
-rw-r--r--plugins/funind/merge.ml8
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.