diff options
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index 12d8e98c4..b830ccefe 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -96,14 +96,14 @@ 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 sigma (_,t) -> head_in indl t gl) c + general_decompose (fun sigma (_,t) -> head_in indl (EConstr.of_constr t) gl) c end } let decompose_and c = |