Small code improvement.

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 79b3743dabbe96035b61ca77f91301b12c9941df..5c42e9ecc1c1072e11bf634616c356ba3982282b 100644 (file)
--- 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
 ;;