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

11 files changed, 50 insertions, 58 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 ->
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 803d197f18..456e89bad9 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -195,23 +195,19 @@ let lowercase_first_char id = String.lowercase (first_char id)
 
 (* id_of_global gives the name of the given sort oper *)
 let id_of_global env = function
-  | Const sp -> 
+  | ConstRef sp -> 
       basename sp
-  | Evar ev ->
-      id_of_string ("?" ^ string_of_int ev)
-  | MutInd (sp,tyi) -> 
+  | IndRef (sp,tyi) -> 
       (* Does not work with extracted inductive types when the first 
 	 inductive is logic : if tyi=0 then basename sp else *)
       let mib = lookup_mind sp env in
       let mip = mind_nth_type_packet mib tyi in
       mip.mind_typename
-  | MutConstruct ((sp,tyi),i) ->
+  | ConstructRef ((sp,tyi),i) ->
       let mib = lookup_mind sp env in
       let mip = mind_nth_type_packet mib tyi in
       assert (i <= Array.length mip.mind_consnames && i > 0);
       mip.mind_consnames.(i-1)
-  | _ -> 
-      assert false
 
 let hdchar env c = 
   let rec hdrec k c =
@@ -228,9 +224,9 @@ let hdchar env c =
 	if i=0 then 
 	  lowercase_first_char (basename sp)
 	else 
-	  let na = id_of_global env (MutInd x) in lowercase_first_char na
+	  let na = id_of_global env (IndRef x) in lowercase_first_char na
     | IsMutConstruct ((sp,i) as x,_) ->
-	let na = id_of_global env (MutConstruct x) in
+	let na = id_of_global env (ConstructRef x) in
 	String.lowercase(List.hd(explode_id na))
     | IsVar id  -> lowercase_first_char id
     | IsSort s -> sort_hdchar s
diff --git a/kernel/environ.mli b/kernel/environ.mli
index e9270c5583..42d560ec90 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -97,7 +97,7 @@ val lookup_constant : section_path -> env -> constant_body
 val lookup_mind : section_path -> env -> mutual_inductive_body
 
 (*s Miscellanous *)
-val id_of_global : env -> sorts oper -> identifier
+val id_of_global : env -> global_reference -> identifier
 
 val make_all_name_different : env -> env
 
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]. *)
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index cbfacf1388..b2b0da9456 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -414,10 +414,9 @@ let print_name name =
   with Not_found -> 
   try 
     match fst (Declare.global_operator CCI name) with
-      | Const sp -> print_constant true " = " sp
-      | MutInd (sp,_) -> print_inductive sp
-      | MutConstruct((sp,_),_) -> print_inductive sp
-      | _ -> assert false
+      | ConstRef sp -> print_constant true " = " sp
+      | IndRef (sp,_) -> print_inductive sp
+      | ConstructRef ((sp,_),_) -> print_inductive sp
   with Not_found -> 
   try
     let (c,typ) = Global.lookup_var name in 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index da78f8352e..b7d38651cb 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -38,10 +38,10 @@ let globpr gt = match gt with
       pr_qualified_path sp (basename (section_path sl s))
   | Node(_,"MUTIND",[Path(_,sl,s); Num(_,tyi)]) ->
       let sp = section_path sl s in
-      pr_qualified_path sp (Global.id_of_global (MutInd (sp,tyi)))
+      pr_qualified_path sp (Global.id_of_global (IndRef (sp,tyi)))
   | Node(_,"MUTCONSTRUCT",[Path(_,sl,s); Num(_,tyi); Num(_,i)]) ->
       let sp = section_path sl s in
-      pr_qualified_path sp (Global.id_of_global (MutConstruct ((sp,tyi),i)))
+      pr_qualified_path sp (Global.id_of_global (ConstructRef ((sp,tyi),i)))
 (*
   | Node(_,"EVAR", (Num (_,ev))::_) ->
       if !print_arguments then dfltpr gt
diff --git a/pretyping/class.ml b/pretyping/class.ml
index 21935be3c7..f9c36315b6 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -443,9 +443,9 @@ let process_coercion sec_sp (((coe,coeinfo),s,t) as x) =
 	if defined_in_sec sp sec_sp then 
 	  let ((_,spid,spk)) = repr_path sp in
 	  let newsp = Lib.make_path spid CCI in
-	  let id = Global.id_of_global (MutConstruct((newsp,i),j)) in
+	  let id = Global.id_of_global (ConstructRef ((newsp,i),j)) in
           (((NAM_Constructor ((newsp,i),j)),coeinfo),s1,t1),id,p
 	else
 	  ((coe,coeinfo),s1,t1),
-	  Global.id_of_global (MutConstruct((sp,i),j)),
+	  Global.id_of_global (ConstructRef ((sp,i),j)),
 	  p
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index d136821a63..477a294b89 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -34,10 +34,9 @@ let interp_modif absfun oper (oper',modif) cl =
   let rec interprec = function
     | ([], cl) -> 
 	(match oper' with
-	   | Const sp -> mkConst (sp,Array.of_list cl)
-	   | MutConstruct sp -> mkMutConstruct (sp,Array.of_list cl)
-	   | MutInd sp -> mkMutInd (sp,Array.of_list cl)
-	   | _ -> anomaly "not a reference operator")
+	   | ConstRef sp -> mkConst (sp,Array.of_list cl)
+	   | ConstructRef sp -> mkMutConstruct (sp,Array.of_list cl)
+	   | IndRef sp -> mkMutInd (sp,Array.of_list cl))
     | (ERASE::tlm, c::cl) -> interprec (tlm,cl)
     | (ABSTRACT::tlm, c::cl) -> absfun (interprec (tlm,cl)) c
     | _ -> assert false
@@ -67,8 +66,8 @@ let modify_opers replfun absfun oper_alist =
       (* Hack pour le sp dans l'annotation du Cases *)
       | OpMutCase (n,(spi,a,b,c,d) as oper) ->
 	  (try
-	     match List.assoc (MutInd spi) oper_alist with
-	       | DO_ABSTRACT (MutInd spi',_) ->
+	     match List.assoc (IndRef spi) oper_alist with
+	       | DO_ABSTRACT (IndRef spi',_) ->
 		   gather_constr (OpMutCase (n,(spi',a,b,c,d)),cl')
 	       | _ -> raise Not_found
 	   with
@@ -76,13 +75,13 @@ let modify_opers replfun absfun oper_alist =
 
       | OpMutInd spi ->
 	  (try
-	     (match List.assoc (MutInd spi) oper_alist with
+	     (match List.assoc (IndRef spi) oper_alist with
 		| NOT_OCCUR -> failure ()
 		| DO_ABSTRACT (oper',modif) ->
 		    if List.length modif > Array.length cl then
 		      anomaly "found a reference with too few args"
 		    else 
-		      interp_modif absfun (MutInd spi) (oper',modif)
+		      interp_modif absfun (IndRef spi) (oper',modif)
 			(Array.to_list cl')
 		| DO_REPLACE -> assert false)
 	   with 
@@ -90,13 +89,13 @@ let modify_opers replfun absfun oper_alist =
 
       | OpMutConstruct spi ->
 	  (try
-	     (match List.assoc (MutConstruct spi) oper_alist with
+	     (match List.assoc (ConstructRef spi) oper_alist with
 		| NOT_OCCUR -> failure ()
 		| DO_ABSTRACT (oper',modif) ->
 		    if List.length modif > Array.length cl then
 		      anomaly "found a reference with too few args"
 		    else 
-		      interp_modif absfun (MutConstruct spi) (oper',modif)
+		      interp_modif absfun (ConstructRef spi) (oper',modif)
 			(Array.to_list cl')
 		| DO_REPLACE -> assert false)
 	   with 
@@ -104,13 +103,13 @@ let modify_opers replfun absfun oper_alist =
 
       | OpConst sp ->
 	  (try
-	     (match List.assoc (Const sp) oper_alist with
+	     (match List.assoc (ConstRef sp) oper_alist with
 		| NOT_OCCUR -> failure ()
 		| DO_ABSTRACT (oper',modif) ->
 		    if List.length modif > Array.length cl then
 		      anomaly "found a reference with too few args"
 		    else 
-		      interp_modif absfun (Const sp) (oper',modif)
+		      interp_modif absfun (ConstRef sp) (oper',modif)
 			(Array.to_list cl')
 		| DO_REPLACE -> substrec (replfun (sp,cl')))
 	   with 
@@ -247,12 +246,12 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
   let (inds',modl) = abstract_inductive ids_to_discard mib.mind_hyps inds in
   let lmodif_one_mind i = 
     let nbc = Array.length (mind_nth_type_packet mib i).mind_consnames in 
-    (MutInd(osecsp,i),DO_ABSTRACT(MutInd(nsecsp,i),modl))::
+    (IndRef (osecsp,i), DO_ABSTRACT (IndRef(nsecsp,i),modl))::
     (list_tabulate
        (function j -> 
 	  let j' = j + 1 in
-	  (MutConstruct((osecsp,i),j'),
-	   DO_ABSTRACT(MutConstruct((nsecsp,i),j'),modl)))
+	  (ConstructRef ((osecsp,i),j'),
+	   DO_ABSTRACT (ConstructRef ((nsecsp,i),j'),modl)))
        nbc) 
   in
   let modifs = List.flatten (list_tabulate lmodif_one_mind mib.mind_ntypes) in 
@@ -270,7 +269,7 @@ let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb =
   let typ = expmod_type oldenv modlist cb.const_type in
   let hyps = map_var_context (expmod_constr oldenv modlist) cb.const_hyps in
   let (body',typ',modl) = abstract_constant ids_to_discard hyps (body,typ) in
-  let mods = [ (Const osecsp, DO_ABSTRACT(Const nsecsp,modl)) ] in
+  let mods = [ (ConstRef osecsp, DO_ABSTRACT(ConstRef nsecsp,modl)) ] in
   (body', body_of_type typ', mods)
 
 
@@ -322,7 +321,7 @@ let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
     | "CONSTANT" | "PARAMETER" ->
 	let stre = constant_or_parameter_strength sp in
 	if stre = (DischargeAt sec_sp) then
-	  (ops, ids_to_discard, (Const sp, DO_REPLACE) :: work_alist)
+	  (ops, ids_to_discard, (ConstRef sp, DO_REPLACE) :: work_alist)
 	else
 	  let cb = Environ.lookup_constant sp oldenv in
 	  let spid = basename sp in