From f20dbafa3e49c35414640e01c3549ad1c802d331 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 3 Dec 1999 09:09:37 +0000
Subject:  - 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
---
 pretyping/recordops.mli | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

(limited to 'pretyping/recordops.mli')

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index d619fd3ae..9b666513f 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
-- 
cgit v1.2.3