diff options
| author | Matthieu Sozeau | 2015-11-28 19:41:17 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-11-28 19:43:26 +0100 |
| commit | 90fef3ffd236f2ed5575b0d11a47185185abc75b (patch) | |
| tree | 2768466af2fc67d61a9e9e94e89fb632d54f3c72 /toplevel/command.ml | |
| parent | 4a11dc25938f3f009e23f1e7c5fe01b2558928c3 (diff) | |
Univs: correctly register universe binders for lemmas.
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 0b709a3fc4..91cfddb547 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1128,7 +1128,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = - List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in + List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) + fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in @@ -1164,7 +1165,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = - List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in + List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) + fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in |