Disparition du type oper mais nouveau type global_reference

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@620 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 12 insertions, 12 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 678bdd8b39..963f418218 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -83,7 +83,7 @@ let resolve_with_bindings_tac  (c,lbind) gl =
 
 let reduce_to_mind gl t = 
   let rec elimrec t l =
-    let c, args = whd_castapp_stack t [] in
+    let c, args = whd_stack t in
     match kind_of_term c, args with
     | (IsMutInd _,_) -> (c,Environ.it_mkProd_or_LetIn t l)
     | (IsConst _,_) -> 
@@ -162,9 +162,9 @@ exception Destruct
 let dest_const_apply t = 
   let f,args = get_applist t in 
   match kind_of_term f with 
-    | IsConst (sp,_) -> 	Global.id_of_global (Const sp),args
-    | IsMutConstruct (csp,_) -> Global.id_of_global (MutConstruct csp),args
-    | IsMutInd (isp,_)       -> Global.id_of_global (MutInd isp),args
+    | IsConst (sp,_) -> 	Global.id_of_global (ConstRef sp),args
+    | IsMutConstruct (csp,_) -> Global.id_of_global (ConstructRef csp),args
+    | IsMutInd (isp,_)       -> Global.id_of_global (IndRef isp),args
     | _ -> raise Destruct 
 
 type result = 
@@ -177,11 +177,11 @@ let destructurate t =
   let c, args = get_applist t in
   match kind_of_term c, args with
     | IsConst (sp,_), args ->
-	Kapp (string_of_id (Global.id_of_global (Const sp)),args)
+	Kapp (string_of_id (Global.id_of_global (ConstRef sp)),args)
     | IsMutConstruct (csp,_) , args ->
-	Kapp (string_of_id (Global.id_of_global (MutConstruct csp)),args)
+	Kapp (string_of_id (Global.id_of_global (ConstructRef csp)),args)
     | IsMutInd (isp,_), args ->
-	Kapp (string_of_id (Global.id_of_global (MutInd isp)),args)
+	Kapp (string_of_id (Global.id_of_global (IndRef isp)),args)
     | IsVar id,[] -> Kvar(string_of_id id)
     | IsProd (Anonymous,typ,body), [] -> Kimp(typ,body)
     | IsProd (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index f5a8746b97..7c514bd2a9 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -103,7 +103,7 @@ let coq_eqT = lazy (constant "#Logic_Type#eqT.cci" "eqT")
 
 module OperSet = 
   Set.Make (struct 
-	      type t = sorts oper
+	      type t = global_reference
 	      let compare = (Pervasives.compare : t->t->int)
 	    end)	
 
@@ -299,7 +299,7 @@ let build_spolynom gl th lc =
   (* aux creates the spolynom p by a recursive destructuration of c 
      and builds the varmap with side-effects *)
   let rec aux c = 
-    match (kind_of_term (whd_castapp c)) with 
+    match (kind_of_term (strip_outer_cast c)) with 
       | IsAppL (binop,[|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
 	  mkAppA [| Lazy.force coq_SPplus; th.th_a; aux c1; aux c2 |]
       | IsAppL (binop,[|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
@@ -353,7 +353,7 @@ let build_polynom gl th lc =
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
   let rec aux c = 
-    match (kind_of_term (whd_castapp c)) with 
+    match (kind_of_term (strip_outer_cast c)) with 
       | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
 	  mkAppA [| Lazy.force coq_Pplus; th.th_a; aux c1; aux c2 |]
       | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
@@ -418,7 +418,7 @@ let build_aspolynom gl th lc =
   (* aux creates the aspolynom p by a recursive destructuration of c 
      and builds the varmap with side-effects *)
   let rec aux c = 
-    match (kind_of_term (whd_castapp c)) with 
+    match (kind_of_term (strip_outer_cast c)) with 
       | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
 	  mkAppA [| Lazy.force coq_ASPplus; aux c1; aux c2 |]
       | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
@@ -469,7 +469,7 @@ let build_apolynom gl th lc =
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
   let rec aux c = 
-    match (kind_of_term (whd_castapp c)) with 
+    match (kind_of_term (strip_outer_cast c)) with 
       | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
 	  mkAppA [| Lazy.force coq_APplus; aux c1; aux c2 |]
       | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->