diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-09-17 09:48:19 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-09-17 09:48:19 +0200 |
| commit | 13ea0a5011875e362aa388989b72b3f7ed0c505b (patch) | |
| tree | faa045035065875845cea1c80cbb3a3b4f624fbf /plugins/funind/merge.ml | |
| parent | f2f805ed8275f70767284f4d3c8a13db6f8c8923 (diff) | |
| parent | fbb3ccdb099170e5a39c9f39512b1ab2503951ea (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'plugins/funind/merge.ml')
| -rw-r--r-- | plugins/funind/merge.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index ea699580b..69e055c23 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 = |