From 1bb57cf59aeaf9fec121804703e25d0478a327d6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 18 Sep 2002 09:24:46 +0000 Subject: [PATCH] Small code improvement. --- helm/gTopLevel/fourierR.ml | 22 ++++++---------------- 1 file changed, 6 insertions(+), 16 deletions(-) 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 ;; -- 2.39.2