- global_reference traite des variables

 - construct_reference, avec environnement en argument
 - link de Class
 - Definition et Check au toplevel


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

3 files changed, 22 insertions, 23 deletions

diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 97ace7b8ab..9816beaa85 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -63,5 +63,4 @@ val ise_resolve_nocheck : 'a evar_map -> (int * constr) list ->
  * Unused outside Trad, but useful for debugging
  *)
 val pretype : 
-  trad_constraint -> env -> 'a evar_defs -> rawconstr 
-    -> unsafe_judgment
+  trad_constraint -> env -> 'a evar_defs -> rawconstr -> unsafe_judgment
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index d619fd3ae7..9b666513f7 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -22,9 +22,9 @@ type struc_typ = {
   s_PARAM : int;
   s_PROJ : section_path option list }
 
-val add_new_struc : Names.section_path * Names.identifier * int *
-    Names.section_path option list -> unit
-val struc_info : Names.section_path -> struc_typ
+val add_new_struc : 
+  section_path * identifier * int * section_path option list -> unit
+val struc_info : section_path -> struc_typ
 
 type obj_typ = {
   o_DEF : constr;
@@ -32,17 +32,18 @@ type obj_typ = {
   o_TPARAMS : constr list; (* dans l'ordre *)
   o_TCOMPS : constr list } (* dans l'ordre *)
                
-val oBJDEFS : ((cte_typ*cte_typ) * obj_typ) list ref
+val oBJDEFS : ((cte_typ * cte_typ) * obj_typ) list ref
 val sTRUCS : (section_path * struc_typ) list ref
 
-val objdef_info : (cte_typ*cte_typ) -> obj_typ
-val add_new_objdef : (Classops.cte_typ * Classops.cte_typ) * Term.constr * Term.constr list *
-    Term.constr list * Term.constr list -> unit
+val objdef_info : (cte_typ * cte_typ) -> obj_typ
+val add_new_objdef : 
+  (Classops.cte_typ * Classops.cte_typ) * Term.constr * Term.constr list *
+  Term.constr list * Term.constr list -> unit
 
 
-val inStruc : section_path*struc_typ -> obj
-val outStruc : obj -> section_path*struc_typ
+val inStruc : section_path * struc_typ -> obj
+val outStruc : obj -> section_path * struc_typ
 val inObjDef1 : section_path -> obj
 val outObjDef1 : obj -> section_path
 
-val add_new_objdef1 : ((cte_typ*cte_typ) * obj_typ) -> unit
+val add_new_objdef1 : ((cte_typ * cte_typ) * obj_typ) -> unit
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 926e2601c2..ce9ea73909 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -19,10 +19,9 @@ val get_type_of_with_meta : env -> 'a evar_map -> metamap -> constr -> constr
 val get_sort_of : env -> 'a evar_map -> constr -> sorts
 
 (*i The following should be merged with mind_specif and put elsewhere 
-    Note : it needs Reduction
-i*)
+    Note : it needs Reduction i*)
 
-(* A light version of mind_specif *)
+(* A light version of [mind_specif] *)
 
 (* Invariant: We have\\
    -- Hnf (fullmind) = DOPN(AppL,[|coremind;..params..;..realargs..|])\\
@@ -30,14 +29,14 @@ i*)
  *)
 type mutind_id = inductive_path * constr array
 
-type mutind =
-    {fullmind : constr;
-     mind : mutind_id;
-     nparams : int;
-     nconstr : int;
-     params : constr list;
-     realargs : constr list;
-     arity : constr};;
+type mutind = {
+  fullmind : constr;
+  mind : mutind_id;
+  nparams : int;
+  nconstr : int;
+  params : constr list;
+  realargs : constr list;
+  arity : constr }
 
 (* [try_mutind_of sigma t] raise Induc if [t] is not an inductive type *)
 val try_mutind_of : env -> 'a Evd.evar_map -> constr -> mutind