diff options
| author | herbelin | 2001-02-05 23:06:33 +0000 |
|---|---|---|
| committer | herbelin | 2001-02-05 23:06:33 +0000 |
| commit | 9759a74e3910ba12608f7bcddd40f7d97247dbcc (patch) | |
| tree | e473ca4d9858ba1316212d17217540e61e7b6ba4 /pretyping/recordops.mli | |
| parent | c9aa1b6d908d3a4f8d9906ba0f11c0bb11569ab7 (diff) | |
Restructuration de classops; évolution en une version mieux intégrée au reste du système; conséquences collatérales
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1327 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/recordops.mli')
| -rwxr-xr-x | pretyping/recordops.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index f82e074baf..097eb25b8a 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -34,9 +34,9 @@ type obj_typ = { o_TPARAMS : constr list; (* dans l'ordre *) o_TCOMPS : constr list } (* dans l'ordre *) -val objdef_info : (cte_typ * cte_typ) -> obj_typ +val objdef_info : (global_reference * global_reference) -> obj_typ val add_new_objdef : - (Classops.cte_typ * Classops.cte_typ) * Term.constr * Term.constr list * + (global_reference * global_reference) * Term.constr * Term.constr list * Term.constr list * Term.constr list -> unit @@ -45,4 +45,4 @@ val outStruc : obj -> inductive_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 : ((global_reference * global_reference) * obj_typ) -> unit |