diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index dbf256ba8..80f3b26e4 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1164,7 +1164,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind 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) + Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC) fixdefs) in let init_tac = Option.map (List.map Proofview.V82.tactic) init_tac @@ -1201,7 +1201,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n 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) + Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC) fixdefs) in let init_tac = Option.map (List.map Proofview.V82.tactic) init_tac |