diff options
| author | ppedrot | 2012-12-14 15:56:25 +0000 |
|---|---|---|
| committer | ppedrot | 2012-12-14 15:56:25 +0000 |
| commit | 67f5c70a480c95cfb819fc68439781b5e5e95794 (patch) | |
| tree | 67b88843ba54b4aefc7f604e18e3a71ec7202fd3 /kernel/declarations.mli | |
| parent | cc03a5f82efa451b6827af9a9b42cee356ed4f8a (diff) | |
Modulification of identifier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 0a09ad76f1..fc142d2532 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -123,13 +123,13 @@ type inductive_arity = type one_inductive_body = { (** {8 Primitive datas } *) - mind_typename : identifier; (** Name of the type: [Ii] *) + mind_typename : Id.t; (** Name of the type: [Ii] *) mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *) mind_arity : inductive_arity; (** Arity sort and original user arity if monomorphic *) - mind_consnames : identifier array; (** Names of the constructors: [cij] *) + mind_consnames : Id.t array; (** Names of the constructors: [cij] *) mind_user_lc : types array; (** Types of the constructors with parameters: [forall params, Tij], @@ -208,8 +208,8 @@ and struct_expr_body = | SEBwith of struct_expr_body * with_declaration_body and with_declaration_body = - With_module_body of identifier list * module_path - | With_definition_body of identifier list * constant_body + With_module_body of Id.t list * module_path + | With_definition_body of Id.t list * constant_body and module_body = { (** absolute path of the module *) |