Restructuration de classops; évolution en une version mieux intégrée au reste du système; conséquences collatérales

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

2 files changed, 28 insertions, 33 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 40ecc11c3..022c75cb6 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -57,9 +57,10 @@ let rec stre_unif_cond = function
 	stre_max (stre1,stre2)
 
 let stre_of_coe = function
-  | NAM_Constant sp -> constant_or_parameter_strength sp
-  | NAM_Section_Variable sp -> variable_strength sp
-  | NAM_Inductive _ | NAM_Constructor _ -> NeverDischarge 
+  | ConstRef sp -> constant_or_parameter_strength sp
+  | VarRef sp -> variable_strength sp
+  | IndRef _ | ConstructRef _ -> NeverDischarge 
+  | EvarRef _ -> anomaly "Not a persistent reference"
 
 (* verfications pour l'ajout d'une classe *)
 
@@ -81,12 +82,12 @@ let try_add_class v (cl,p) streopt check_exist =
   if check_exist & class_exists cl then
     errorlabstrm "try_add_new_class" 
       [< 'sTR (string_of_class cl) ; 'sTR " is already a class" >];
-  let stre' = stre_of_cl cl in 
+  let stre' = strength_of_cl cl in 
   let stre = match streopt with
     | Some stre -> stre_max (stre,stre')
     | None -> stre'
   in
-  add_new_class (cl,stre,p);
+  declare_class (cl,stre,p);
   stre
 
 (* try_add_new_class : Names.identifier -> unit *)
@@ -112,8 +113,8 @@ let try_add_new_class ref stre =
 let check_class v cl p =
   try 
     let _,clinfo = class_info cl in
-    check_fully_applied cl p clinfo.cL_PARAM;
-    clinfo.cL_STRE
+    check_fully_applied cl p clinfo.cl_param;
+    clinfo.cl_strength
   with Not_found -> 
     let env = Global.env () in
     let t = Retyping.get_type_of env Evd.empty v in
@@ -143,14 +144,14 @@ let check_target clt = function
 (* t provient de global_reference donc pas de Cast, pas de App *)
 let coe_of_reference t = 
   match kind_of_term t with
-    | IsConst (sp,l) -> (Array.to_list l),NAM_Constant sp
-    | IsMutInd (ind_sp,l) -> (Array.to_list l),NAM_Inductive ind_sp
-    | IsMutConstruct (cstr_sp,l) -> (Array.to_list l),NAM_Constructor cstr_sp
+    | IsConst (sp,l) -> (Array.to_list l), ConstRef sp
+    | IsMutInd (ind_sp,l) -> (Array.to_list l), IndRef ind_sp
+    | IsMutConstruct (cstr_sp,l) -> (Array.to_list l), ConstructRef cstr_sp
     | IsVar id  ->
 	let sp =
 	  try find_section_variable id 
 	  with Not_found -> anomaly "Not a reference"
-	in [],NAM_Section_Variable sp
+	in [], VarRef sp
     |  _ -> anomaly "Not a reference"
 
 let constructor_at_head1 t = 
@@ -299,13 +300,6 @@ let build_id_coercion idf_opt source =
   let sp = declare_constant idf (constr_entry,NeverDischarge,false) in
   ConstRef sp
 
-let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) ps =
-  add_anonymous_leaf
-    (inCoercion
-       ((coef,
-	 {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}),
-	cls,clt))
-
 (* 
 nom de la fonction coercion
 strength de f
@@ -369,7 +363,7 @@ let try_add_new_coercion_core idf stre source target isid =
      'sTR" must be declared as a local coercion (its strength is ";
      'sTR(string_of_strength stre');'sTR")" >] *)
   let stre = stre_max (stre,stre') in
-  add_new_coercion_in_graph1 (coef,vj,stre,isid,cls,clt) ps
+  declare_coercion coef vj stre isid cls clt ps
 
 
 let try_add_new_coercion ref stre =
@@ -404,7 +398,7 @@ let count_extra_abstractions hyps ids_to_discard =
 let defined_in_sec sp sec_sp = dirpath sp = sec_sp
 
 let process_class sec_sp ids_to_discard x =
-  let (cl,{cL_STRE=stre; cL_PARAM=p}) = x in
+  let (cl,{cl_strength=stre; cl_param=p}) = x in
 (*  let env = Global.env () in*)
   match cl with 
     | CL_SECVAR _ -> x
@@ -419,7 +413,7 @@ let process_class sec_sp ids_to_discard x =
           let t = Retyping.get_type_of env Evd.empty v in
           let p = arity_sort t in
 *)
-          (CL_CONST newsp,{cL_STRE=stre;cL_PARAM=p+n})
+          (CL_CONST newsp,{cl_strength=stre;cl_param=p+n})
         else 
 	  x
     | CL_IND (sp,i) ->
@@ -433,7 +427,7 @@ let process_class sec_sp ids_to_discard x =
           let t = Retyping.get_type_of env Evd.empty v in
           let p = arity_sort t in
 *)
-          (CL_IND (newsp,i),{cL_STRE=stre;cL_PARAM=p+n})
+          (CL_IND (newsp,i),{cl_strength=stre;cl_param=p+n})
         else 
 	  x
     | _ -> anomaly "process_class" 
@@ -463,25 +457,26 @@ let process_coercion sec_sp (((coe,coeinfo),s,t) as x) =
   let s1= process_cl sec_sp s in
   let t1 = process_cl sec_sp t in
   match coe with 
-    | NAM_Section_Variable _ -> ((coe,coeinfo),s1,t1)
-    | NAM_Constant sp -> 
+    | VarRef _ -> ((coe,coeinfo),s1,t1)
+    | ConstRef sp -> 
 	if defined_in_sec sp sec_sp then
 	  let ((_,spid,spk)) = repr_path sp in
 	  let newsp = Lib.make_path spid CCI in
-	  ((NAM_Constant newsp,coeinfo),s1,t1)
+	  ((ConstRef newsp,coeinfo),s1,t1)
 	else
 	  ((coe,coeinfo),s1,t1)
-    | NAM_Inductive (sp,i) -> 
+    | IndRef (sp,i) -> 
 	if defined_in_sec sp sec_sp then
 	  let ((_,spid,spk)) = repr_path sp in
 	  let newsp = Lib.make_path spid CCI in
-	  ((NAM_Inductive (newsp,i),coeinfo),s1,t1)
+	  ((IndRef (newsp,i),coeinfo),s1,t1)
 	else
 	  ((coe,coeinfo),s1,t1)
-    | NAM_Constructor ((sp,i),j) -> 
+    | ConstructRef ((sp,i),j) -> 
 	if defined_in_sec sp sec_sp then 
 	  let ((_,spid,spk)) = repr_path sp in
 	  let newsp = Lib.make_path spid CCI in
-          (((NAM_Constructor ((newsp,i),j)),coeinfo),s1,t1)
+          (((ConstructRef ((newsp,i),j)),coeinfo),s1,t1)
 	else
 	  ((coe,coeinfo),s1,t1)
+    | EvarRef _ -> anomaly "No Evar expected here as coercion"
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 8b8279a6a..a3c9586a4 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -216,7 +216,7 @@ let process_object oldenv dir sec_sp
 
     | "CLASS" -> 
 	let ((cl,clinfo) as x) = outClass lobj in
-	if clinfo.cL_STRE = (DischargeAt sec_sp) then 
+	if clinfo.cl_strength = (DischargeAt sec_sp) then 
 	  (ops,ids_to_discard,work_alist)
 	else
 	  let (y1,y2) = process_class sec_sp ids_to_discard x in
@@ -224,7 +224,7 @@ let process_object oldenv dir sec_sp
 	  
     | "COERCION" -> 
 	let (((_,coeinfo),_,_)as x) = outCoercion lobj in
-        if coeinfo.cOE_STRE = (DischargeAt sec_sp) then 
+        if coercion_strength coeinfo = (DischargeAt sec_sp) then 
 	  (ops,ids_to_discard,work_alist)
         else
 	  let y = process_coercion sec_sp x in
@@ -298,8 +298,8 @@ let push_inductive_names ccitab sp mie =
 (*s Operations performed at section closing. *)
 
 let cache_end_section (_,(sp,mc)) =
-  Nametab.push_module sp mc;
-  Nametab.open_module_contents (qualid_of_sp sp)
+  Nametab.push_section sp mc;
+  Nametab.open_section_contents (qualid_of_sp sp)
 
 let load_end_section (_,(sp,mc)) =
   Nametab.push_module sp mc