diff options
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index 3f0c01a29..12d8e98c4 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -79,11 +79,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 } @@ -102,17 +103,17 @@ let head_in indl t gl = 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 @@ -133,7 +134,7 @@ let induction_trailer abs_i abs_j bargs = (fun id -> Proofview.Goal.nf_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) (EConstr.of_constr idty) in let possible_bring_hyps = (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums in |