diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/inv.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 0ff6b69a5c..dc88795216 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -123,6 +123,7 @@ let make_inv_predicate env evd indf realargs id status concl = let refl_term = eqdata.Coqlib.refl in let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in let refl = mkApp (refl_term, [|eqnty; rhs|]) in + let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd refl in let args = refl :: args in build_concl eqns args (succ n) restlist in |