From fb83ea501028d0b43e36df3eb01958f3f3d3cf75 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 1 Apr 2003 13:50:33 +0000
Subject: Extension de Replace aux égalités entre preuves

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3833 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 27fffec56f..3c3b6e7cf9 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -131,12 +131,7 @@ let abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl =
   let t1 = pf_type_of gl c1 
   and t2 = pf_type_of gl c2 in
   if unsafe or (pf_conv_x gl t1 t2) then
-    let (e,sym) = 
-      match kind_of_term (hnf_type_of gl t1) with 
-        | Sort (Prop(Pos)) -> (eq,sym_eq)
-        | Sort (Type(_))   -> (eq,sym_eq)
-        | _                  -> error "replace"
-    in 
+    let (e,sym) = (eqt,sym_eqt) in
     (tclTHENLAST (elim_type (applist (e, [t1;c1;c2])))
        (tclORELSE assumption 
           (tclTRY (tclTHEN (apply sym) assumption)))) gl
-- 
cgit v1.2.3