diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 3d91877d0..0a0589e96 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -369,7 +369,7 @@ let general_elim_then_using match predicate with | None -> elimclause' | Some p -> - clenv_unify true Evd.CONV (mkMeta pmv) p elimclause' + clenv_unify true Reduction.CONV (mkMeta pmv) p elimclause' in elim_res_pf_THEN_i elimclause' branchtacs gl |