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

3 files changed, 9 insertions, 11 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 0393f54237..6b45dedb0d 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -223,22 +223,22 @@ let first f v =
   look_for 0
 
 let mind_oper_of_id sp id mib =
-  first 
+  first
     (fun tyi mip ->
        if id = mip.mind_typename then 
-	 MutInd (sp,tyi)
+	 IndRef (sp,tyi)
        else
 	 first 
 	   (fun cj cid -> 
 	      if id = cid then 
-		MutConstruct((sp,tyi),succ cj) 
+		ConstructRef ((sp,tyi),succ cj) 
 	      else raise Not_found) 
 	   mip.mind_consnames)
     mib.mind_packets
 
 let global_sp_operator env sp id =
   try
-    let cb = Environ.lookup_constant sp env in Const sp, cb.const_hyps
+    let cb = Environ.lookup_constant sp env in ConstRef sp, cb.const_hyps
   with Not_found -> 
     let mib = Environ.lookup_mind sp env in
     mind_oper_of_id sp id mib, mib.mind_hyps
@@ -287,10 +287,9 @@ let construct_sp_reference env sp id =
   let env0 = Environ.reset_context env in
   let args = List.map mkVar (ids_of_var_context hyps) in
   let body = match oper with
-    | Const sp -> mkConst (sp,Array.of_list args)
-    | MutConstruct sp -> mkMutConstruct (sp,Array.of_list args)
-    | MutInd sp -> mkMutInd (sp,Array.of_list args)
-    | _ -> assert false
+    | ConstRef sp -> mkConst (sp,Array.of_list args)
+    | ConstructRef sp -> mkMutConstruct (sp,Array.of_list args)
+    | IndRef sp -> mkMutInd (sp,Array.of_list args)
   in
   find_common_hyps_then_abstract body env0 hyps0 hyps
 
@@ -351,7 +350,6 @@ let elimination_suffix = function
   | Prop Pos  -> "_rec"
 
 let declare_eliminations sp i =
-  let oper = MutInd (sp,i) in
   let mib = Global.lookup_mind sp in
   let ids = ids_of_var_context mib.mind_hyps in
   if not (list_subset ids (ids_of_var_context (Global.var_context ()))) then
diff --git a/library/declare.mli b/library/declare.mli
index f078c91661..4a33500fc7 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -58,7 +58,7 @@ val variable_strength : identifier -> strength
     construtor) corresponding to [id] in global environment, together
     with its definition environment. *)
 
-val global_operator : path_kind -> identifier -> sorts oper * var_context
+val global_operator : path_kind -> identifier -> global_reference * var_context
 
 (*s [global_reference k id] returns the object corresponding to
     the name [id] in the global environment. It may be a constant, 
diff --git a/library/global.mli b/library/global.mli
index b51ce3c774..4a993d1aaa 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -48,7 +48,7 @@ val import : compiled_env -> unit
 
 (*s Some functions of [Environ] instanciated on the global environment. *)
 
-val id_of_global : sorts oper -> identifier
+val id_of_global : global_reference -> identifier
 
 (*s Re-exported functions of [Inductive], composed with 
     [lookup_mind_specif]. *)