diff options
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 46 |
1 files changed, 25 insertions, 21 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index f2b9eec4..003b069b 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -1,22 +1,25 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util open Names -open Term open Termops +open EConstr open Inductiveops open Hipattern open Tacmach.New open Tacticals.New open Tactics open Proofview.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* Supposed to be called without as clause *) let introElimAssumsThen tac ba = @@ -76,16 +79,17 @@ 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 tclTHENS (cut typc) [ tclTHEN (intro_using tmphyp_name) (onLastHypId - (ifOnHyp recognizer (general_decompose_aux recognizer) + (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 @@ -94,24 +98,24 @@ let head_in indl t gl = let ity,_ = if !up_to_delta then find_mrectype env sigma t - else extract_mrectype t + else extract_mrectype sigma t in List.exists (fun i -> eq_ind (fst i) (fst ity)) indl 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 (_,t) -> head_in indl t gl) c - end } + general_decompose (fun sigma (_,t) -> head_in indl t gl) c + end let decompose_and c = general_decompose - (fun (_,t) -> is_record t) + (fun sigma (_,t) -> is_record sigma t) c let decompose_or c = general_decompose - (fun (_,t) -> is_disjunction t) + (fun sigma (_,t) -> is_disjunction sigma t) c let h_decompose l c = decompose_these c l @@ -130,16 +134,16 @@ let induction_trailer abs_i abs_j bargs = (tclDO (abs_j - abs_i) intro) (onLastHypId (fun id -> - Proofview.Goal.nf_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) idty in + let fvty = global_vars (pf_env gl) (project gl) idty in let possible_bring_hyps = (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums in let (hyps,_) = List.fold_left (fun (bring_ids,leave_ids) d -> - let cid = get_id d in + let cid = NamedDecl.get_id d in if not (List.mem cid leave_ids) then (d::bring_ids,leave_ids) else (bring_ids,cid::leave_ids)) @@ -148,11 +152,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.nf_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 = @@ -165,7 +169,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 |