From fc403f2f912cfceef5ff96af379b6e9d912f0c03 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 9 Nov 2003 15:12:54 +0000
Subject: Traduction semantique des InHyp de clause en InHypValue si local def;
 simplification suite fusion eq/eqT

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4840 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.ml | 11 +++--------
 1 file changed, 3 insertions(+), 8 deletions(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index b537d5e689..2649d21d4e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -189,11 +189,8 @@ let necessary_elimination sort_arity sort =
             (str "no primitive equality on proofs")
 
 let find_eq_pattern aritysort sort = 
-  match necessary_elimination aritysort sort with
-    | Set_Type       -> (build_coq_eq_data ()).eq
-    | Type_Type      -> (build_coq_idT_data ()).eq
-    | Set_SetorProp  -> (build_coq_eq_data ()).eq
-    | Type_SetorProp -> (build_coq_eq_data ()).eq
+  (* "eq" now accept arguments in Type and elimination to Type *)
+  Coqlib.build_coq_eq ()
 
 (* [find_positions t1 t2]
 
@@ -1157,9 +1154,7 @@ let unfold_body x gl =
           (pr_id x ++ str" is not a defined hypothesis") in
   let aft = afterHyp x gl in
   let hl = List.fold_right
-    (fun (y,yval,_) cl ->
-      if yval=None then InHypType y :: cl
-      else InHyp y :: InHypType y :: cl) aft [] in
+    (fun (y,yval,_) cl -> (y,(InHyp,ref None)) :: cl) aft [] in
   let xvar = mkVar x in
   let rfun _ _ c = replace_term xvar xval c in
   tclTHENLIST
-- 
cgit v1.2.3