diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-03 09:09:37 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-03 09:09:37 +0000 |
| commit | f20dbafa3e49c35414640e01c3549ad1c802d331 (patch) | |
| tree | 761e97154851e214a6d6802c9decb977bfa1b07e /pretyping/recordops.mli | |
| parent | 4318eefacae280fed3a159acfede35c568b2942b (diff) | |
- 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
Diffstat (limited to 'pretyping/recordops.mli')
| -rwxr-xr-x | pretyping/recordops.mli | 21 |
1 files changed, 11 insertions, 10 deletions
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 |