From e27949240f5b1ee212e7d0fe3326a21a13c4abb0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 17:21:44 +0100 Subject: Typing API using EConstr. --- tactics/inv.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics/inv.ml') diff --git a/tactics/inv.ml b/tactics/inv.ml index 38f75995b..9282af759 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -123,13 +123,13 @@ 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.type_of env) evd refl in + let _ = Evarutil.evd_comb1 (Typing.type_of env) evd (EConstr.of_constr refl) in let args = refl :: args in build_concl eqns args (succ n) restlist in let (newconcl, args) = build_concl [] [] 0 realargs in let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in - let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in + let _ = Evarutil.evd_comb1 (Typing.type_of env) evd (EConstr.of_constr predicate) in (* OK - this predicate should now be usable by res_elimination_then to do elimination on the conclusion. *) predicate, args -- cgit v1.2.3