diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index fb7237e4b2..ea74dc37ea 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -165,10 +165,10 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = in List.map try_occ occs let instantiate_lemma gl c ty l l2r concl = - let ct = pf_unsafe_type_of gl c in - let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in - let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in - [eqclause] + let sigma, ct = pf_type_of gl c in + let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in + let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in + [eqclause] let rewrite_conv_closed_core_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; |