From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 02:12:40 +0100 Subject: Evar-normalizing functions now act on EConstrs. --- tactics/contradiction.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'tactics/contradiction.ml') diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index a3a448aad..7173fb4fd 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -66,8 +66,7 @@ let contradiction_context = | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction") | d :: rest -> let id = NamedDecl.get_id d in - let typ = nf_evar sigma (NamedDecl.get_type d) in - let typ = EConstr.of_constr typ in + let typ = nf_evar sigma (EConstr.of_constr (NamedDecl.get_type d)) in let typ = whd_all env sigma typ in if is_empty_type sigma typ then simplest_elim (mkVar id) -- cgit v1.2.3