diff options
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index 3f0c01a29..e37ec6bce 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -10,6 +10,7 @@ open Util open Names open Term open Termops +open EConstr open Inductiveops open Hipattern open Tacmach.New @@ -79,11 +80,12 @@ let up_to_delta = ref false (* true *) let general_decompose recognizer c = Proofview.Goal.enter { 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 } @@ -95,24 +97,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 -> let indl = List.map (fun x -> x, Univ.Instance.empty) l in - general_decompose (fun (_,t) -> head_in indl t gl) c + 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 @@ -131,9 +133,9 @@ 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 { 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 @@ -153,7 +155,7 @@ let induction_trailer abs_i abs_j bargs = )) let double_ind h1 h2 = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { 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 = |