From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 18 Sep 2002 09:24:46 +0000 (+0000)
Subject: Small code improvement.
X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~70
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1bb57cf59aeaf9fec121804703e25d0478a327d6;p=helm.git

Small code improvement.
---

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 79b3743da..5c42e9ecc 100644
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -548,19 +548,6 @@ let tac_use h = match h.htype with
 
 
 
-(* servono tutti ????????????????????????? *)
-let uri_of_term t =
-  match t with 
-  Cic.Const(u,_) -> u
-  |Cic.Var(u) -> u
-  |Cic.MutInd(u,_,_) -> u
-  |Cic.MutConstruct(u,_,_,_) -> u
-  |Cic.MutCase(u,_,_,_,_,_) -> u
-  | _ -> UriManager.uri_of_string "??????" 
- ;;
-
-
-
 let is_ineq (h,t) =
     match t with
        Cic.Appl ( Cic.Const(u,boh)::next) ->
@@ -569,9 +556,12 @@ let is_ineq (h,t) =
 		|"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
 		|"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
 		|"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
-		|"cic:/Coq/Init/Logic_Type/eqT.con" -> (match (UriManager.string_of_uri (uri_of_term(List.hd next))) with
-                            "cic:/Coq/Reals/Rdefinitions/R.con"->true
-			    |_->false)
+		|"cic:/Coq/Init/Logic_Type/eqT.con" ->
+                   (match (List.hd next) with
+                       Cic.Const (uri,_) when
+                        UriManager.string_of_uri uri =
+                        "cic:/Coq/Reals/Rdefinitions/R.con" -> true
+                     | _ -> false)
                 |_->false)
      |_->false
 ;;