diff options
| author | Maxime Dénès | 2017-04-27 17:30:54 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-27 17:30:54 +0200 |
| commit | 338f8df5ea59a46b60fcfbe50e122fd6eee0dc52 (patch) | |
| tree | ac27debb6849cab3e637205578901a92b70a51df /vernac | |
| parent | 0bfd1f2a461ec989dbe812b10d8ee39d296bc777 (diff) | |
| parent | 6d4f2222aa7ff6039f9f386cbc38201a0cd60c08 (diff) | |
Merge PR#568: Remove tactic compatibility layer
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/command.ml | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index 45ff579552..b27d8a0a35 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -1198,11 +1198,8 @@ 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 (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC) + Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in - let init_tac = - Option.map (List.map Proofview.V82.tactic) init_tac - in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint) evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) @@ -1235,11 +1232,8 @@ 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 (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC) + Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in - let init_tac = - Option.map (List.map Proofview.V82.tactic) init_tac - in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) |