From 3c36e46caf34e5033ba9378674caee0efa93d809 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 28 Oct 2013 14:16:53 +0000 Subject: Evar leak in "absurd" tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16943 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/contradiction.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'tactics') diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index d6e51a15d..fbd5a8cb0 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -20,20 +20,20 @@ open Misctypes let absurd c gls = let env = pf_env gls and sigma = project gls in - let _,j = Coercion.inh_coerce_to_sort Loc.ghost env - (Evd.create_goal_evar_defs sigma) (Retyping.get_judgment_of env sigma c) in + let j = Retyping.get_judgment_of env sigma c in + let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in let c = j.Environ.utj_val in (tclTHENS (tclTHEN (elim_type (build_coq_False ())) (cut c)) ([(tclTHENS - (cut (applist(build_coq_not (),[c]))) + (cut (mkApp(build_coq_not (),[|c|]))) ([(tclTHEN intros ((fun gl -> let ida = pf_nth_hyp_id gl 1 and idna = pf_nth_hyp_id gl 2 in - exact_no_check (applist(mkVar idna,[mkVar ida])) gl))); + exact_no_check (mkApp(mkVar idna,[|mkVar ida|])) gl))); tclIDTAC])); - tclIDTAC])) gls + tclIDTAC])) { gls with Evd.sigma; } (* Contradiction *) -- cgit v1.2.3