diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-28 12:36:20 -0400 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-28 12:42:00 -0400 |
| commit | 0132b5b51fc1856356fb74130d3dea7fd378f76c (patch) | |
| tree | da5c0ec53dcecafb2fab5db1a112fac8b6311e60 /plugins/funind/merge.ml | |
| parent | 89be9efbf6dbd8a04fb8ccab4c9aa7a11b9a0f03 (diff) | |
Univs: local names handling.
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
Diffstat (limited to 'plugins/funind/merge.ml')
| -rw-r--r-- | plugins/funind/merge.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 60c58730a..e3455e770 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -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. *) |