diff options
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index 855cb206f..13d64b8e3 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -77,7 +77,7 @@ let tmphyp_name = Id.of_string "_TmpHyp" let up_to_delta = ref false (* true *) let general_decompose recognizer c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let type_of = pf_unsafe_type_of gl in let sigma = project gl in let typc = type_of c in @@ -87,7 +87,7 @@ let general_decompose recognizer c = (ifOnHyp (recognizer sigma) (general_decompose_aux (recognizer sigma)) (fun id -> clear [id]))); exact_no_check c ] - end } + end let head_in indl t gl = let env = Proofview.Goal.env gl in @@ -101,10 +101,10 @@ let head_in indl t gl = with Not_found -> false let decompose_these c l = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let indl = List.map (fun x -> x, Univ.Instance.empty) l in general_decompose (fun sigma (_,t) -> head_in indl t gl) c - end } + end let decompose_and c = general_decompose @@ -132,7 +132,7 @@ let induction_trailer abs_i abs_j bargs = (tclDO (abs_j - abs_i) intro) (onLastHypId (fun id -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let idty = pf_unsafe_type_of gl (mkVar id) in let fvty = global_vars (pf_env gl) (project gl) idty in let possible_bring_hyps = @@ -150,11 +150,11 @@ let induction_trailer abs_i abs_j bargs = let ids = List.rev (ids_of_named_context hyps) in (tclTHENLIST [revert ids; simple_elimination (mkVar id)]) - end } + end )) let double_ind h1 h2 = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let abs_i = depth_of_quantified_hypothesis true h1 gl in let abs_j = depth_of_quantified_hypothesis true h2 gl in let abs = @@ -167,7 +167,7 @@ let double_ind h1 h2 = (fun id -> elimination_then (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) - end } + end let h_double_induction = double_ind |