From 83407b72d17ec5b84ef5830a32288313fbfb9bd6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 8 Sep 2005 12:24:35 +0000
Subject: Réparation bug #1004; nettoyage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7351 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.ml  | 4 ----
 tactics/equality.mli | 2 --
 tactics/inv.ml       | 3 +--
 3 files changed, 1 insertion(+), 8 deletions(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 30a01d6a98..0ef96e5fef 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -172,10 +172,6 @@ let build_rect eq =
 	  
 (*********** List of constructions depending of the initial state *)
 
-let find_eq_pattern aritysort sort = 
-  (* "eq" now accept arguments in Type and elimination to Type *)
-  Coqlib.build_coq_eq ()
-
 (* [find_positions t1 t2]
 
    will find the positions in the two terms which are suitable for
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 4afdfe757c..fc7c3828ea 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -24,8 +24,6 @@ open Tacexpr
 open Rawterm
 (*i*)
 
-val find_eq_pattern : sorts -> sorts -> constr
-
 val general_rewrite_bindings : bool -> constr with_bindings -> tactic
 val general_rewrite          : bool -> constr -> tactic
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 4609c360ee..75cb667783 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -134,9 +134,8 @@ let make_inv_predicate env sigma indf realargs id status concl =
           else 
 	    make_iterated_tuple env' sigma ai (xi,ti)
 	in
-        let type_type_rhs = get_sort_of env sigma (type_of env sigma rhs) in
         let sort = get_sort_of env sigma concl in 
-        let eq_term = find_eq_pattern type_type_rhs sort in
+        let eq_term = Coqlib.build_coq_eq () in
         let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in 
 	build_concl ((Anonymous,lift n eqn)::eqns) (n+1) restlist
   in
-- 
cgit v1.2.3