diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 45 |
1 files changed, 21 insertions, 24 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e792585822..9c2a1d8509 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2811,20 +2811,18 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl = mkProd_or_LetIn decl cl', sigma' let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = - let env = Tacmach.pf_env gl in - let ids = Tacmach.pf_ids_of_hyps gl in - let sigma, t = Typing.type_of env sigma c in - generalize_goal_gen env sigma ids i o t cl - -let new_generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = - let env = Tacmach.New.pf_env gl in - let ids = Tacmach.New.pf_ids_of_hyps gl in + let open Tacmach.New in + let env = pf_env gl in + let ids = pf_ids_of_hyps gl in let sigma, t = Typing.type_of env sigma c in generalize_goal_gen env sigma ids i o t cl -let old_generalize_dep ?(with_let=false) c gl = +let generalize_dep ?(with_let=false) c = + let open Tacmach.New in + let open Tacticals.New in + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let env = pf_env gl in - let sign = pf_hyps gl in + let sign = Proofview.Goal.hyps gl in let sigma = project gl in let init_ids = ids_of_named_context (Global.named_context()) in let seek (d:named_declaration) (toquant:named_context) = @@ -2843,11 +2841,11 @@ let old_generalize_dep ?(with_let=false) c gl = -> id::tothin | _ -> tothin in - let cl' = it_mkNamedProd_or_LetIn (Tacmach.pf_concl gl) to_quantify in + let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in let body = if with_let then match EConstr.kind sigma c with - | Var id -> id |> Tacmach.pf_get_hyp gl |> NamedDecl.get_value + | Var id -> id |> (fun id -> pf_get_hyp id gl) |> NamedDecl.get_value | _ -> None else None in @@ -2856,20 +2854,19 @@ let old_generalize_dep ?(with_let=false) c gl = (** Check that the generalization is indeed well-typed *) let (evd, _) = Typing.type_of env evd cl'' in let args = Context.Named.to_instance mkVar to_quantify_rev in - tclTHENLIST - [tclEVARS evd; - Proofview.V82.of_tactic (apply_type cl'' (if Option.is_empty body then c::args else args)); - Proofview.V82.of_tactic (clear (List.rev tothin'))] - gl - -let generalize_dep ?(with_let = false) c = - Proofview.V82.tactic (old_generalize_dep ~with_let c) + let tac = + tclTHEN + (apply_type cl'' (if Option.is_empty body then c::args else args)) + (clear (List.rev tothin')) + in + Sigma.Unsafe.of_pair (tac, evd) + end } (** *) let generalize_gen_let lconstr = Proofview.Goal.s_enter { s_enter = begin fun gl -> let env = Proofview.Goal.env gl in let newcl, evd = - List.fold_right_i (new_generalize_goal gl) 0 lconstr + List.fold_right_i (generalize_goal gl) 0 lconstr (Tacmach.New.pf_concl gl,Tacmach.New.project gl) in let (evd, _) = Typing.type_of env evd newcl in @@ -4724,7 +4721,7 @@ let symmetry_red allowred = | Some eq_data,_,_ -> Tacticals.New.tclTHEN (convert_concl_no_check concl DEFAULTcast) - (Tacticals.New.pf_constr_of_global eq_data.sym apply) + (Tacticals.New.pf_constr_of_global eq_data.sym >>= apply) | None,eq,eq_kind -> prove_symmetry eq eq_kind end } @@ -4820,8 +4817,8 @@ let transitivity_red allowred t = Tacticals.New.tclTHEN (convert_concl_no_check concl DEFAULTcast) (match t with - | None -> Tacticals.New.pf_constr_of_global eq_data.trans eapply - | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t])) + | None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply + | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t]) | None,eq,eq_kind -> match t with | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.") |