module Classops; ajout de fonctions dans Declare en consequence

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

3 files changed, 267 insertions, 296 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 0bb314d40d..f69253eea8 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -1,148 +1,139 @@
-(* $Id$ *)
 
-open Util;;
-open Pp;;
-open Names;;
-open Vartab;;
-open Libobject;;
-open Constrtypes;;
-open List;;
-open Library;;
-open Term;;
-open Generic;;
-open Initial;;
+(* $Id$ *)
 
+open Util
+open Pp
+open Options
+open Names
+open Environ
+open Libobject
+open Declare
+open Term
+open Generic
 
 (* usage qque peu general: utilise aussi dans record *)
 
-type cte_typ = NAM_Var of identifier | NAM_SP of section_path | NAM_Construct of section_path*int*int
-;;
+type cte_typ = 
+  | NAM_Var of identifier 
+  | NAM_SP of section_path 
+  | NAM_Construct of section_path*int*int
 
 let cte_of_constr = function  
-    (DOPN(Const sp,l)) -> NAM_SP sp
-  | (DOPN(MutInd (sp,_),l)) -> NAM_SP sp
-  | (VAR(id)) -> NAM_Var id
-  | (DOPN(MutConstruct ((sp,i),j) ,l)) -> NAM_Construct (sp,i,j)
+  | DOPN(Const sp,_) -> NAM_SP sp
+  | DOPN(MutInd (sp,_),_) -> NAM_SP sp
+  | VAR id -> NAM_Var id
+  | DOPN(MutConstruct ((sp,i),j) ,_) -> NAM_Construct (sp,i,j)
   |  _ -> raise Not_found
-;;
 
-type cl_typ = CL_SORT | CL_FUN | CL_Var of identifier | CL_SP of section_path 
-            | CL_IND of section_path*int
-;;
+type cl_typ = 
+  | CL_SORT 
+  | CL_FUN
+  | CL_Var of identifier
+  | CL_SP of section_path 
+  | CL_IND of section_path * int
 
-type cl_info_typ = {cL_STR : string;
-                    cL_STRE : strength;
-                    cL_PARAM : int}
-;;
+type cl_info_typ = {
+  cL_STR : string;
+  cL_STRE : strength;
+  cL_PARAM : int }
 
 type coe_typ = cte_typ
-;;
 
-type coe_info_typ = {cOE_VALUE : judgement;
-                     cOE_STRE : strength;
-                     cOE_ISID : bool;
-                     cOE_PARAM : int}
-;;
+type coe_info_typ = {
+  cOE_VALUE : unsafe_judgment;
+  cOE_STRE : strength;
+  cOE_ISID : bool;
+  cOE_PARAM : int }
 
 type inheritance_path = int list
-;;
+
 
 (* table des classes, des coercions et graphe d'heritage *)
 
-let cLASSES = (ref [] : (int * (cl_typ * cl_info_typ)) list ref);;
+let cLASSES = (ref [] : (int * (cl_typ * cl_info_typ)) list ref)
 
-let cOERCIONS = (ref [] : (int * (coe_typ * coe_info_typ)) list ref);;
+let cOERCIONS = (ref [] : (int * (coe_typ * coe_info_typ)) list ref)
 
-let iNHERITANCE_GRAPH = (ref [] : ((int * int) * inheritance_path) list ref);; 
+let iNHERITANCE_GRAPH = (ref [] : ((int * int) * inheritance_path) list ref) 
 
-let freeze () = (!cLASSES,!cOERCIONS,
-                 !iNHERITANCE_GRAPH)
-;;
+let freeze () = (!cLASSES,!cOERCIONS, !iNHERITANCE_GRAPH)
 
-let unfreeze (fcl,fco,fig) = (cLASSES:=fcl;
-                              cOERCIONS:=fco;
-                              iNHERITANCE_GRAPH:=fig)
-;;
+let unfreeze (fcl,fco,fig) = 
+  cLASSES:=fcl;
+  cOERCIONS:=fco;
+  iNHERITANCE_GRAPH:=fig
 
 (* ajout de nouveaux "objets" *)
 
 let newNum_class = 
  let num = ref 0 in
  function () -> (num:=!num+1;!num)
-;;
 
 let newNum_coercion = 
  let num = ref 0 in
  function () -> (num:=!num+1;!num)
-;;
 
 let add_new_class_num (n,(cl,s)) = 
-cLASSES := (n,(cl,s))::(!cLASSES)
-;;
+  cLASSES := (n,(cl,s))::(!cLASSES)
 
 let add_new_class1 (cl,s) = 
-add_new_class_num (newNum_class(),(cl,s))
-;;
+  add_new_class_num (newNum_class(),(cl,s))
 
 let add_new_coercion_num (n,(coe,s)) = 
-cOERCIONS := (n,(coe,s))::(!cOERCIONS)
-;;
+  cOERCIONS := (n,(coe,s))::(!cOERCIONS)
 
 let add_new_coercion (coe,s) = 
-let n = newNum_coercion() in 
-add_new_coercion_num (n,(coe,s));n
-;;
+  let n = newNum_coercion() in 
+  add_new_coercion_num (n,(coe,s));n
 
 let add_new_path x =
-iNHERITANCE_GRAPH := x::(!iNHERITANCE_GRAPH)
-;;
+  iNHERITANCE_GRAPH := x::(!iNHERITANCE_GRAPH)
 
-let init () = (cLASSES:= []; 
-               add_new_class1 (CL_FUN,{cL_STR="FUNCLASS";cL_PARAM=0;cL_STRE=NeverDischarge});
-               add_new_class1 (CL_SORT,{cL_STR="SORTCLASS";cL_PARAM=0;cL_STRE=NeverDischarge});
-               cOERCIONS:= [];
-               iNHERITANCE_GRAPH:= [])
-;;
+let init () = 
+  cLASSES:= []; 
+  add_new_class1 (CL_FUN,{cL_STR="FUNCLASS";
+			  cL_PARAM=0;cL_STRE=NeverDischarge});
+  add_new_class1 (CL_SORT,{cL_STR="SORTCLASS";
+			   cL_PARAM=0;cL_STRE=NeverDischarge});
+  cOERCIONS:= [];
+  iNHERITANCE_GRAPH:= []
 
-init();;
+let _ = init()
 
 (* fonction de recherche *)
 
 let search_info x l = 
-let rec aux = function [] -> raise Not_found
-                     | (n,(x1,r))::l -> if x=x1 then (n,r)
-                                        else aux l
-in aux l
-;;
+  let rec aux = function 
+    | [] -> raise Not_found
+    | (n,(x1,r))::l -> if x=x1 then (n,r) else aux l
+  in 
+  aux l
 
 (* class_info : cl_typ -> int * cl_info_typ *)
 
 let class_info cl = search_info cl (!cLASSES)
-;;
 
 (* class_info_from_index : int -> cl_typ * cl_info_typ *)
 
 let class_info_from_index i = List.assoc i (!cLASSES)
-;;
 
 (* coercion_info : coe_typ -> int * coe_info_typ *)
 
 let coercion_info coe = search_info coe (!cOERCIONS)
-;;
 
 (* coercion_info_from_index : int -> coe_typ * coe_info_typ *)
 
-let coercion_info_from_index i = List.assoc i (!cOERCIONS)
-;;
+let coercion_info_from_index i = 
+  List.assoc i (!cOERCIONS)
 
-let lookup_path_between (s,t) = List.assoc (s,t) (!iNHERITANCE_GRAPH);;
+let lookup_path_between (s,t) =
+  List.assoc (s,t) (!iNHERITANCE_GRAPH)
 
-let lookup_path_to_fun_from s = lookup_path_between (s,fst(class_info CL_FUN))
-;;
-
-let lookup_path_to_sort_from s = lookup_path_between (s,fst(class_info CL_SORT))
-;;
+let lookup_path_to_fun_from s = 
+  lookup_path_between (s,fst(class_info CL_FUN))
 
+let lookup_path_to_sort_from s = 
+  lookup_path_between (s,fst(class_info CL_SORT))
 
 (* library, summary *)
 
@@ -150,228 +141,213 @@ let lookup_path_to_sort_from s = lookup_path_between (s,fst(class_info CL_SORT))
  val outClass : Libobject.object -> (cl_typ * cl_info_typ) = <fun> *)
 
 let (inClass,outClass) =
-    declare_object ("CLASS",
-                    {load_function = (fun _ -> ());
-                     cache_function = (function  (_,x) -> add_new_class1 x);
-                     specification_function = (function x -> x)});;
+  declare_object ("CLASS",
+                  { load_function = (fun _ -> ());
+		    open_function = (fun _ -> ());
+                    cache_function = (function  (_,x) -> add_new_class1 x);
+                    specification_function = (function x -> x) })
 
 let add_new_class (cl,s,stre,p) = 
-add_anonymous_object (inClass ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p})))
-;;
-
-Library.declare_summary "inh_graph"
-{Summary.freeze_function = freeze;
- Summary.unfreeze_function = unfreeze;
- Summary.init_function = init}
-;;
+  Lib.add_anonymous_leaf (inClass ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p})))
+    
+let _ = 
+  Summary.declare_summary "inh_graph"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init }
 
 (* classe d'un terme *)
 
 (* constructor_at_head : constr -> cl_typ * int *)
 
 let constructor_at_head t = 
-let rec aux t' = match t' with
-    (DOPN(Const sp,_)) -> CL_SP sp,0
-  | (DOPN(MutInd (sp,i),_)) -> CL_IND (sp,i),0
-  | (VAR(id)) -> CL_Var id,0
-  | (DOP2(Cast,c,_)) -> aux (collapse_appl c)
-  | (DOPN(AppL,cl)) -> let c,_ = aux (hd_vect cl) 
-                        in c,Array.length(cl)-1
-  | DOP2(Prod,_,DLAM(_,c)) -> CL_FUN,0
-  | DOP0(Sort(_)) -> CL_SORT,0
-  |  _ -> raise Not_found
-in aux (collapse_appl t)
-;;
+  let rec aux t' = match t' with
+    | (DOPN(Const sp,_)) -> CL_SP sp,0
+    | (DOPN(MutInd (sp,i),_)) -> CL_IND (sp,i),0
+    | (VAR(id)) -> CL_Var id,0
+    | (DOP2(Cast,c,_)) -> aux (collapse_appl c)
+    | (DOPN(AppL,cl)) -> 
+	let c,_ = aux (array_hd cl) in c,Array.length(cl)-1
+    | DOP2(Prod,_,DLAM(_,c)) -> CL_FUN,0
+    | DOP0(Sort(_)) -> CL_SORT,0
+    |  _ -> raise Not_found
+  in 
+  aux (collapse_appl t)
 
 (* class_of : Term.constr -> int *)
 
-
-let class_of sigma t = 
-let t,n,n1,i = (try let (cl,n) = constructor_at_head t in
-               let (i,{cL_PARAM=n1}) = class_info cl in
-               t,n,n1,i              
-              with _ -> let t = Reduction.hnf_constr sigma t in
-                        let (cl,n) = constructor_at_head t in
-                        let (i,{cL_PARAM=n1}) = class_info cl in
-                        t,n,n1,i) in
-if n = n1 then t,i 
-else raise Not_found
-;;
-
-(*
-
-let class_of t = 
-let (cl,n) = constructor_at_head t in
-let (i,{cL_PARAM=n1}) = class_info cl in
-if n = n1 then i 
-else raise Not_found
-;;
-*)
+let class_of env sigma t = 
+  let t,n,n1,i = 
+    (try 
+       let (cl,n) = constructor_at_head t in
+       let (i,{cL_PARAM=n1}) = class_info cl in
+       t,n,n1,i              
+     with _ -> 
+       let t = Tacred.hnf_constr env sigma t in
+       let (cl,n) = constructor_at_head t in
+       let (i,{cL_PARAM=n1}) = class_info cl in
+       t,n,n1,i) 
+  in
+  if n = n1 then t,i else raise Not_found
 
 let rec class_args_of c = 
-let aux = function (DOP2(Cast,c,_)) -> class_args_of c
-                 | (DOPN(AppL,cl)) -> Array.to_list(tl_vect(cl))
-                 | _ -> []
-in aux (collapse_appl c)
-;;
+  let aux = function 
+    | (DOP2(Cast,c,_)) -> class_args_of c
+    | (DOPN(AppL,cl)) -> Array.to_list(array_tl cl)
+    | _ -> []
+  in 
+  aux (collapse_appl c)
 
 (* verfications pour l'ajout d'une classe *)
 
 let fully_applied id p p1 =
-if p <> p1
-then  errorlabstrm "fully_applied" 
-          [< 'sTR"Wrong number of parameters for ";'sTR(string_of_id id) >]
-;;
+  if p <> p1 then  errorlabstrm "fully_applied" 
+    [< 'sTR"Wrong number of parameters for ";'sTR(string_of_id id) >]
 
 let rec arity_sort = function
-    DOP0(Sort(Prop(_))) -> 0
+  | DOP0(Sort(Prop(_))) -> 0
   | DOP0(Sort(Type(_))) -> 0
   | DOP2(Prod,_,DLAM(_,c)) -> (arity_sort c) +1
   | DOP2(Cast,c,_) -> arity_sort c
   | _ -> raise Not_found
-;;
-
-let stre_of_cl = 
-  function CL_SP sp ->
-                    (match Lib.leaf_object_tag (objsp_of sp) with
-                      "CONSTANT" ->
-                       let (_,stre,_) = Environ.outConstant(Lib.map_leaf (objsp_of sp)) in stre
-                      | _ -> NeverDischarge)
-          | CL_Var id -> stre_of_var id
-          | _ -> NeverDischarge
-;;
+
+let stre_of_cl = function 
+  | CL_SP sp ->
+      if is_constant sp then constant_strength sp else NeverDischarge
+  | CL_Var id -> 
+      variable_strength id
+  | _ -> NeverDischarge
 
 (* coe_value : int -> Term.constr * bool *)
 
 let coe_value i = 
-let (_,{cOE_VALUE=v;cOE_ISID=b}) = coercion_info_from_index i in
-v,b
-;;
+  let (_,{cOE_VALUE=v;cOE_ISID=b}) = coercion_info_from_index i in
+  v,b
 
-(* fonction de print *)
+(* pretty-print functions *)
 
-let string_of_strength = function NeverDischarge -> "(global)"
-                                | DischargeAt sp -> "(disch@"^(string_of_path sp)
-;;
+open Printer
 
-let print_coercion_value v = (prterm v.cOE_VALUE._VAL);;
+let string_of_strength = function 
+  | NeverDischarge -> "(global)"
+  | DischargeAt sp -> "(disch@"^(string_of_path sp)
 
-let print_index_coercion c = 
- let _,v = coercion_info_from_index c in
- print_coercion_value v;;
+let print_coercion_value v = prterm v.cOE_VALUE.uj_val
 
-(*
-let string_of_cl = function CL_Var id -> string_of_id id
-                          | CL_SP sp -> string_of_id (basename sp)
-                          | CL_IND (sp,i,s) -> s
-                          | CL_FUN -> "FUNCLASS"
-                          | CL_SORT -> "SORTCLASS";;
-*)
+let print_index_coercion c = 
+  let _,v = coercion_info_from_index c in
+  print_coercion_value v
 
 let print_class i =
- let cl,x = class_info_from_index i in
- [< 'sTR x.cL_STR >];;
-
-let print_path ((i,j),p) = [< 'sTR"["; 
-                                   prlist_with_sep (fun () -> [< 'sTR"; " >])
-                                   (fun c ->  print_index_coercion c) p;
-                                   'sTR"] : "; print_class i; 'sTR" >-> ";
-                                   print_class j >];;
+  let cl,x = class_info_from_index i in
+  [< 'sTR x.cL_STR >]
+  
+let print_path ((i,j),p) = 
+  [< 'sTR"["; 
+     prlist_with_sep (fun () -> [< 'sTR"; " >])
+       (fun c ->  print_index_coercion c) p;
+     'sTR"] : "; print_class i; 'sTR" >-> ";
+     print_class j >]
 
 let print_graph () = 
-  [< prlist_with_sep pr_fnl print_path (!iNHERITANCE_GRAPH) >];;
+  [< prlist_with_sep pr_fnl print_path (!iNHERITANCE_GRAPH) >]
 
 let print_classes () = 
   [< prlist_with_sep pr_spc
-     (fun (_,(cl,x)) -> 
-        [< 'sTR x.cL_STR  (*; 'sTR(string_of_strength x.cL_STRE) *) >]) 
-        (!cLASSES) >];;
+       (fun (_,(cl,x)) -> 
+          [< 'sTR x.cL_STR  (*; 'sTR(string_of_strength x.cL_STRE) *) >]) 
+       (!cLASSES) >]
 
 let print_coercions () = 
   [< prlist_with_sep pr_spc
-     (fun (_,(_,v)) -> [< (print_coercion_value v)
-              (* ;'sTR(string_of_strength v.cOE_STRE)*) >]) (!cOERCIONS) >];;
-
+       (fun (_,(_,v)) -> [< print_coercion_value v >]) (!cOERCIONS) >]
+  
 let cl_of_id id = 
-match (string_of_id id) with
- "FUNCLASS" -> CL_FUN
-| "SORTCLASS" -> CL_SORT
-| _ -> let v = Machops.global (gLOB(initial_sign())) id in
-       let cl,_ = constructor_at_head v in cl
-;;
+  match string_of_id id with
+    | "FUNCLASS" -> CL_FUN
+    | "SORTCLASS" -> CL_SORT
+    | _ -> let v = Declare.global_reference CCI id in
+	   let cl,_ = constructor_at_head v in 
+	   cl
 
 let index_cl_of_id id =
-try let cl = cl_of_id id in
-    let i,_=class_info cl in i
-with _ -> errorlabstrm "index_cl_of_id"
-          [< 'sTR(string_of_id id); 'sTR" is not a defined class" >]
-;;
+  try 
+    let cl = cl_of_id id in
+    let i,_=class_info cl in 
+    i
+  with _ -> 
+    errorlabstrm "index_cl_of_id"
+      [< 'sTR(string_of_id id); 'sTR" is not a defined class" >]
 
 let print_path_between ids idt = 
-let i = (index_cl_of_id ids) in
-let j = (index_cl_of_id idt) in
-let p = (try lookup_path_between (i,j) 
-         with _ -> errorlabstrm "index_cl_of_id"
-           [< 'sTR"No path between ";'sTR(string_of_id ids); 'sTR" and ";'sTR(string_of_id ids) >]) in
-print_path ((i,j),p);;
+  let i = (index_cl_of_id ids) in
+  let j = (index_cl_of_id idt) in
+  let p = 
+    try 
+      lookup_path_between (i,j) 
+    with _ -> 
+      errorlabstrm "index_cl_of_id"
+        [< 'sTR"No path between ";'sTR(string_of_id ids); 
+	   'sTR" and ";'sTR(string_of_id ids) >]
+  in
+  print_path ((i,j),p)
 
 (* rajouter une coercion dans le graphe *)
  
 let message_ambig l =
-    [< 'sTR"Ambiguous paths : ";
-       prlist_with_sep pr_fnl (fun ijp -> print_path ijp) l >];;
+  [< 'sTR"Ambiguous paths : ";
+     prlist_with_sep pr_fnl (fun ijp -> print_path ijp) l >]
 
 (* add_coercion_in_graph : int * int * int -> unit 
                          coercion,source,target *)
 
 let add_coercion_in_graph (ic,source,target) =
-let old_iNHERITANCE_GRAPH = (!iNHERITANCE_GRAPH) in
-let ambig_paths = (ref []:((int * int) * inheritance_path) list ref) in
-
-let try_add_new_path (p,i,j) =
-    try (if i=j 
-         then (if (snd (class_info_from_index i)).cL_PARAM > 0
-               then (lookup_path_between (i,j);
-                     ambig_paths := ((i,j),p)::!ambig_paths))
-         else
-          (lookup_path_between (i,j);
-          ambig_paths := ((i,j),p)::!ambig_paths);false)
-    with Not_found -> (add_new_path ((i,j),p);true)
-in
-let try_add_new_path1 (p,i,j) = (try_add_new_path (p,i,j);())
-in
-        (if try_add_new_path ([ic],source,target)
-           then 
-             (iter (fun ((s,t),p) ->
-                if s<>t 
-                then ((if (t = source)
-                       then begin
-                            try_add_new_path1 (p @ [ ic ],s,target);
-                            (iter (fun ((u,v),q) ->
-                                    if u<>v 
-                                    then if (u = target) & (p <> q)
-                                         then try_add_new_path1 (p @ [ ic ] @ q,s,v))
-                                              old_iNHERITANCE_GRAPH)
-                            end);
-                       if (s = target)
-                       then try_add_new_path1 (ic::p,source,t)))
-                 old_iNHERITANCE_GRAPH);
-
-if ((!ambig_paths) <> []) & is_mes_ambig()
-then pPNL (message_ambig (!ambig_paths)))
-;;
-
+  let old_iNHERITANCE_GRAPH = !iNHERITANCE_GRAPH in
+  let ambig_paths = (ref []:((int * int) * inheritance_path) list ref) in
+  let try_add_new_path (p,i,j) =
+    try 
+      if i=j then begin
+	if (snd (class_info_from_index i)).cL_PARAM > 0 then begin
+	  let _ = lookup_path_between (i,j) in
+          ambig_paths := ((i,j),p)::!ambig_paths
+	end
+      end else begin
+        let _ = lookup_path_between (i,j) in
+        ambig_paths := ((i,j),p)::!ambig_paths
+      end;
+      false
+    with Not_found -> begin
+      add_new_path ((i,j),p);
+      true
+    end
+  in
+  let try_add_new_path1 (p,i,j) = 
+    let _ = try_add_new_path (p,i,j) in () 
+  in
+  if try_add_new_path ([ic],source,target) then begin
+    List.iter 
+      (fun ((s,t),p) ->
+         if s<>t then begin
+	   if t = source then begin
+             try_add_new_path1 (p @ [ ic ],s,target);
+             List.iter 
+	       (fun ((u,v),q) ->
+                  if u<>v & (u = target) & (p <> q) then 
+		    try_add_new_path1 (p @ [ ic ] @ q,s,v))
+               old_iNHERITANCE_GRAPH
+           end;
+           if s = target then try_add_new_path1 (ic::p,source,t)
+	 end)
+      old_iNHERITANCE_GRAPH 
+  end;
+  if ((!ambig_paths) <> []) & is_mes_ambig() then 
+    pPNL (message_ambig (!ambig_paths))
 
 let add_new_coercion_in_graph ((coef,xf),cls,clt) =
-let is,_ = class_info cls in
-let it,_ = class_info clt in
-let jf = add_new_coercion (coef,xf) in
-add_coercion_in_graph (jf,is,it)
-;;
-
-
-
-
+  let is,_ = class_info cls in
+  let it,_ = class_info clt in
+  let jf = add_new_coercion (coef,xf) in
+  add_coercion_in_graph (jf,is,it)
 
 (* val inCoercion : (coe_typ * coe_info_typ) * cl_typ * cl_typ  ->
                     -> Libobject.object 
@@ -379,10 +355,9 @@ add_coercion_in_graph (jf,is,it)
                          * cl_typ * cl_typ *)
 
 let (inCoercion,outCoercion) =
-    declare_object ("COERCION",
-                    {load_function = (fun _ -> ());
-                     cache_function =
-                       (function  (_,x) -> add_new_coercion_in_graph x);
-                     specification_function = (function x -> x)});;
-
-
+  declare_object ("COERCION",
+                  { load_function = (fun _ -> ());
+		    open_function = (fun _ -> ());
+                    cache_function =
+                      (function  (_,x) -> add_new_coercion_in_graph x);
+                    specification_function = (function x -> x) })
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 98716046f2..25163f6e6a 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -45,7 +45,7 @@ val cte_of_constr : constr -> cte_typ
 val class_info : cl_typ -> (int * cl_info_typ)
 val coercion_info : coe_typ -> (int * coe_info_typ)
 val constructor_at_head : constr -> cl_typ * int
-val class_of :  'c evar_map -> constr -> constr * int
+val class_of : unsafe_env -> 'c evar_map -> constr -> constr * int
 val class_args_of : constr -> constr list
 val inClass : (cl_typ * cl_info_typ) -> obj
 val outClass : obj -> (cl_typ * cl_info_typ)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 3cb03ae53e..9f858ed1df 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -1,27 +1,26 @@
-(* $Id$ *)
 
-open Util;;
-open Pp;;
-open Names;;
-open Typeops;;
-open Vartab;;
-open Libobject;;
-open List;;
-open Library;;
-open Term;;
-open Pp_control;;
-open Generic;;
-open Initial;;
-open Classops;;
+(* $Id$ *)
 
+open Util
+open Pp
+open Names
+open Typeops
+open Vartab
+open Libobject
+open Library
+open Term
+open Pp_control
+open Generic
+open Initial
+open Classops
 
-let nbimpl = ref 0;;
-let nbpathc = ref 0;;
-let nbcoer = ref 0;;
-let nbstruc = ref 0;;
-let nbimplstruc = ref 0;;
+let nbimpl = ref 0
+let nbpathc = ref 0
+let nbcoer = ref 0
+let nbstruc = ref 0
+let nbimplstruc = ref 0
 
-let compter = ref false;;
+let compter = ref false
 
 
 (*** table des structures: section_path du struc donne l'id du constructeur,
@@ -29,25 +28,25 @@ let compter = ref false;;
 
 type struc_typ = {s_CONST : identifier; 
                   s_PARAM : int;
-                  s_PROJ : section_path option list};;
+                  s_PROJ : section_path option list}
 
-let sTRUCS = (ref [] : (section_path * struc_typ) list ref);;
+let sTRUCS = (ref [] : (section_path * struc_typ) list ref)
 
 let add_new_struc1 x = sTRUCS:=x::(!sTRUCS)
-;;
+
 
 let (inStruc,outStruc) =
     declare_object ("STRUCTURE",
                     {load_function = (fun _ -> ());
                      cache_function = (function  (_,x) -> add_new_struc1 x);
-                     specification_function = (function x -> x)});;
+                     specification_function = (function x -> x)})
 
 let add_new_struc (s,c,n,l) = 
 add_anonymous_object (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l}))
-;;
+
 
 let struc_info s = assoc s !sTRUCS
-;;
+
 
 (*** table des definitions "object" : pour chaque object c,
 c := [x1:B1]...[xk:Bk](R_Cons a1...am t1...t_n)
@@ -64,32 +63,32 @@ type obj_typ = {o_DEF : constr;
                 o_TABS : constr list; (* dans l'ordre *)
                 o_TPARAMS : constr list; (* dans l'ordre *)
                 o_TCOMPS : constr list (* dans l'ordre *)
-               };;
+               }
 
-let oBJDEFS = (ref [] : ((cte_typ*cte_typ) * obj_typ) list ref);;
+let oBJDEFS = (ref [] : ((cte_typ*cte_typ) * obj_typ) list ref)
 
 let add_new_objdef1 x = oBJDEFS:=x::(!oBJDEFS)
-;;
+
 
 let (inObjDef,outObjDef) =
     declare_object ("OBJDEF",
                     {load_function = (fun _ -> ());
                      cache_function = (function  (_,x) -> add_new_objdef1 x);
-                     specification_function = (function x -> x)});;
+                     specification_function = (function x -> x)})
 
 let add_new_objdef (o,c,la,lp,l) =
   try let _ = assoc o !oBJDEFS in ()
   with Not_found -> 
     add_anonymous_object 
       (inObjDef (o,{o_DEF=c;o_TABS=la;o_TPARAMS=lp;o_TCOMPS=l}))
-;;
+
 
 
 let ((inObjDef1:section_path -> obj),(outObjDef1:obj -> section_path)) =
     declare_object ("OBJDEF1",
                     {load_function = (fun _ -> ());
                      cache_function = (function  (_,sp) -> ());
-                     specification_function = (function x -> x)});;
+                     specification_function = (function x -> x)})
 
 
 (* let objdef_info (o1,o2) = 
@@ -98,26 +97,23 @@ let ((inObjDef1:section_path -> obj),(outObjDef1:obj -> section_path)) =
                                      else if (o2,o1) = x then Right(y)
                                           else aux l
   in aux !oBJDEFS
-;;
+
 *)
 
-let objdef_info o = assoc o !oBJDEFS;;
+let objdef_info o = assoc o !oBJDEFS
 
 let freeze () = !sTRUCS,!oBJDEFS
-;;
 
-let unfreeze (s,o) = sTRUCS:=s;oBJDEFS:=o
-;;
 
-let init () = sTRUCS:=[];oBJDEFS:=[]
-;;
+let unfreeze (s,o) = sTRUCS:=s;oBJDEFS:=o
 
-init();;
 
+let init () = sTRUCS:=[];oBJDEFS:=[]
 
+let _ = init()
 
-Library.declare_summary "objdefs"
-{Summary.freeze_function = freeze;
- Summary.unfreeze_function = unfreeze;
- Summary.init_function = init}
-;;
+let _ = 
+  Library.declare_summary "objdefs"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init }