From 2ea9a0b938edb872eb2f7bbaabc05ba8ed39295e Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 24 Oct 2006 13:01:55 +0000
Subject: Insère une coercion vers Sortclass dans 'contradiction' si nécessaire
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9269 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/contradiction.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index dd1c68af9..d50477316 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -22,6 +22,10 @@ open Rawterm
 (* Absurd *)
 
 let absurd c gls =
+  let env = pf_env gls and sigma = project gls in
+  let _,j = Coercion.Default.inh_coerce_to_sort dummy_loc env
+    (Evd.create_evar_defs sigma) (Retyping.get_judgment_of env sigma c) in
+  let c = j.Environ.utj_val in
   (tclTHENS
      (tclTHEN (elim_type (build_coq_False ())) (cut c)) 
      ([(tclTHENS
-- 
cgit v1.2.3