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

12 files changed, 339 insertions, 321 deletions

diff --git a/.depend b/.depend
index 4e69fa2f22..2890602a5c 100644
--- a/.depend
+++ b/.depend
@@ -60,8 +60,9 @@ parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
 parsing/g_minicoq.cmi: kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
     kernel/term.cmi 
 parsing/pcoq.cmi: parsing/coqast.cmi 
-parsing/pretty.cmi: kernel/inductive.cmi library/lib.cmi kernel/names.cmi \
-    lib/pp.cmi kernel/term.cmi 
+parsing/pretty.cmi: kernel/environ.cmi kernel/inductive.cmi library/lib.cmi \
+    kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
+    kernel/term.cmi 
 parsing/printer.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi 
 parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi kernel/sign.cmi \
@@ -338,9 +339,9 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
 library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
     library/summary.cmi 
 parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \
-    parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi 
+    kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi 
 parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \
-    parsing/pcoq.cmi lib/pp.cmx lib/util.cmx parsing/ast.cmi 
+    kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx lib/util.cmx parsing/ast.cmi 
 parsing/astterm.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/environ.cmi \
     kernel/evd.cmi kernel/generic.cmi toplevel/himsg.cmi kernel/names.cmi \
     parsing/pcoq.cmi lib/pp.cmi parsing/printer.cmi pretyping/rawterm.cmi \
@@ -359,14 +360,16 @@ parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmi \
     lib/gmap.cmx lib/gmapl.cmx lib/pp.cmx lib/util.cmx parsing/esyntax.cmi 
 parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi 
 parsing/lexer.cmx: lib/util.cmx parsing/lexer.cmi 
-parsing/pretty.cmo: kernel/evd.cmi kernel/generic.cmi library/lib.cmi \
-    library/library.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    parsing/printer.cmi kernel/reduction.cmi kernel/term.cmi \
-    parsing/pretty.cmi 
-parsing/pretty.cmx: kernel/evd.cmx kernel/generic.cmx library/lib.cmx \
-    library/library.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
-    parsing/printer.cmx kernel/reduction.cmx kernel/term.cmx \
-    parsing/pretty.cmi 
+parsing/pretty.cmo: kernel/evd.cmi kernel/generic.cmi library/global.cmi \
+    library/impargs.cmi kernel/inductive.cmi library/lib.cmi \
+    library/libobject.cmi library/library.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi parsing/printer.cmi kernel/reduction.cmi \
+    kernel/sign.cmi kernel/term.cmi lib/util.cmi parsing/pretty.cmi 
+parsing/pretty.cmx: kernel/evd.cmx kernel/generic.cmx library/global.cmx \
+    library/impargs.cmx kernel/inductive.cmx library/lib.cmx \
+    library/libobject.cmx library/library.cmx kernel/names.cmx \
+    library/nametab.cmx lib/pp.cmx parsing/printer.cmx kernel/reduction.cmx \
+    kernel/sign.cmx kernel/term.cmx lib/util.cmx parsing/pretty.cmi 
 parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
     parsing/esyntax.cmi parsing/extend.cmi library/global.cmi \
     kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
@@ -387,12 +390,14 @@ parsing/termast.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
     library/impargs.cmx kernel/inductive.cmx kernel/names.cmx \
     library/nametab.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/univ.cmx lib/util.cmx parsing/termast.cmi 
-pretyping/classops.cmo: kernel/environ.cmi kernel/generic.cmi library/lib.cmi \
-    library/libobject.cmi library/library.cmi kernel/names.cmi lib/pp.cmi \
-    kernel/reduction.cmi kernel/term.cmi lib/util.cmi pretyping/classops.cmi 
-pretyping/classops.cmx: kernel/environ.cmx kernel/generic.cmx library/lib.cmx \
-    library/libobject.cmx library/library.cmx kernel/names.cmx lib/pp.cmx \
-    kernel/reduction.cmx kernel/term.cmx lib/util.cmx pretyping/classops.cmi 
+pretyping/classops.cmo: library/declare.cmi kernel/environ.cmi \
+    kernel/generic.cmi library/lib.cmi library/libobject.cmi kernel/names.cmi \
+    lib/options.cmi lib/pp.cmi parsing/printer.cmi library/summary.cmi \
+    proofs/tacred.cmi kernel/term.cmi lib/util.cmi pretyping/classops.cmi 
+pretyping/classops.cmx: library/declare.cmx kernel/environ.cmx \
+    kernel/generic.cmx library/lib.cmx library/libobject.cmx kernel/names.cmx \
+    lib/options.cmx lib/pp.cmx parsing/printer.cmx library/summary.cmx \
+    proofs/tacred.cmx kernel/term.cmx lib/util.cmx pretyping/classops.cmi 
 pretyping/coercion.cmo: pretyping/classops.cmi kernel/environ.cmi \
     pretyping/evarconv.cmi kernel/evd.cmi kernel/generic.cmi kernel/names.cmi \
     pretyping/recordops.cmi kernel/reduction.cmi kernel/term.cmi \
diff --git a/Makefile b/Makefile
index 35d04737de..d4fd64fbd8 100644
--- a/Makefile
+++ b/Makefile
@@ -59,11 +59,15 @@ TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
 	tactics/wcclausenv.cmo tactics/tacticals.cmo \
         tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo
 
-PRETYPING=pretyping/astterm.cmo
+PRETYPING=pretyping/classops.cmo pretyping/recordops.cmo \
+          pretyping/evarutil.cmo pretyping/evarconv.cmo \
+          pretyping/pretype_errors.cmo pretyping/coercion.cmo \
+	  pretyping/multcase.cmo pretyping/pretyping.cmo
 
 PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
 	parsing/g_prim.cmo parsing/g_basevernac.cmo parsing/g_vernac.cmo \
-	parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo
+	parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo\
+        parsing/printer.cmo parsing/pretty.cmo parsing/astterm.cmo
 
 TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \
          toplevel/vernac.cmo toplevel/mltop.cmo \
@@ -80,6 +84,14 @@ CMX=$(CMO:.cmo=.cmx)
 
 world: minicoq coqtop.byte dev/db_printers.cmo
 
+kernel: $(KERNEL)
+library: $(LIBRARY)
+proofs: $(PROOFS)
+tactics: $(TACTICS)
+parsing: $(PARSING)
+pretyping: $(PRETYPING)
+toplevel: $(TOPLEVEL)
+
 # coqtop
 
 coqtop: $(CMX)
@@ -215,6 +227,8 @@ archclean::
 	rm -f proofs/*.cmx proofs/*.[so]
 	rm -f tactics/*.cmx tactics/*.[so]
 	rm -f parsing/*.cmx parsing/*.[so]
+	rm -f pretyping/*.cmx pretyping/*.[so]
+	rm -f toplevel/*.cmx toplevel/*.[so]
 
 cleanall:: archclean
 	rm -f *~
@@ -226,6 +240,8 @@ cleanall:: archclean
 	rm -f proofs/*.cm[io] proofs/*~
 	rm -f tactics/*.cm[io] tactics/*~
 	rm -f parsing/*.cm[io] parsing/*.ppo parsing/*~
+	rm -f pretyping/*.cm[io] pretyping/*~
+	rm -f toplevel/*.cm[io] toplevel/*~
 
 cleanconfig::
 	rm -f config/Makefile config/coq_config.ml
diff --git a/dev/TODO b/dev/TODO
index 356f1e5b60..563d0d1a13 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -3,9 +3,6 @@
      - conserver les constantes dans leur section de définition
        et redéfinir des constantes déchargées à la sortie
 
- o Variables existentielles
-     - unifier Meta et Evar
-
  o Lib
      - écrire une fonction d'export qui supprimme les FrozenState,
        vérifie qu'il n'y a pas de section ouverte, et présente les
diff --git a/lib/options.ml b/lib/options.ml
index e0cebb1ebb..c4afa1e390 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -32,4 +32,12 @@ let set_print_hyps_limit n = print_hyps_limit := Some n
 let unset_print_hyps_limit () = print_hyps_limit := None
 let print_hyps_limit () = !print_hyps_limit
 
-
+let mes_ambig = ref true
+let make_mes_ambig flag = mes_ambig:=flag
+let is_mes_ambig() = !mes_ambig
+
+let without_mes_ambig f x =
+  let old = is_mes_ambig() in
+  try make_mes_ambig false;
+      let rslt = f x in (make_mes_ambig old; rslt)
+  with e -> (make_mes_ambig old; raise e)
diff --git a/lib/options.mli b/lib/options.mli
index c159767aec..528226360e 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -18,3 +18,7 @@ val set_print_hyps_limit : int -> unit
 val unset_print_hyps_limit : unit -> unit
 val print_hyps_limit : unit -> int option
 
+val make_mes_ambig : bool -> unit
+val is_mes_ambig : unit -> bool
+val without_mes_ambig : ('a -> 'b) -> 'a -> 'b
+
diff --git a/library/declare.ml b/library/declare.ml
index 52355a7e28..909895612e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -135,6 +135,14 @@ let declare_mind mie =
   push_inductive_names sp mie;
   declare_inductive_implicits sp
 
+(* Test and access functions. *)
+
+let is_constant sp = failwith "TODO"
+let constant_strength sp = failwith "TODO"
+
+let is_variable id = failwith "TODO"
+let variable_strength id = failwith "TODO"
+
 (* Global references. *)
 
 let first f v =
diff --git a/library/declare.mli b/library/declare.mli
index 9b0f969820..1b3b842cfb 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -31,6 +31,14 @@ val declare_mind : mutual_inductive_entry -> unit
 val declare_eliminations : section_path -> unit
 
 
+(*s Corresponding test and access functions. *)
+
+val is_constant : section_path -> bool
+val constant_strength : section_path -> strength
+
+val is_variable : identifier -> bool
+val variable_strength : identifier -> strength
+
 (*s It also provides a function [global_reference] to construct a global
   constr (a constant, an inductive or a constructor) from an identifier.
   To do so, it first looks for the section path using [Nametab.sp_of_id] and
diff --git a/library/redinfo.ml b/library/redinfo.ml
index 4e6c202156..dd1f32bd13 100644
--- a/library/redinfo.ml
+++ b/library/redinfo.ml
@@ -74,7 +74,7 @@ let constant_eval sp =
     v
   end
 
-(* Registration as global tables and roolback. *)
+(* Registration as global tables and rollback. *)
 
 type frozen = constant_evaluation Spmap.t
 
diff --git a/parsing/ast.ml b/parsing/ast.ml
index 7b15a0f418..18758d8ae3 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -3,6 +3,7 @@
 
 open Pp
 open Util
+open Names
 open Coqast
 open Pcoq
 
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 }