diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
| commit | 67f5c70a480c95cfb819fc68439781b5e5e95794 (patch) | |
| tree | 67b88843ba54b4aefc7f604e18e3a71ec7202fd3 /checker/declarations.ml | |
| 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 'checker/declarations.ml')
| -rw-r--r-- | checker/declarations.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index df0134e02..7e368dcad 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -607,7 +607,7 @@ type one_inductive_body = { (* Primitive datas *) (* Name of the type: [Ii] *) - mind_typename : identifier; + mind_typename : Id.t; (* Arity context of [Ii] with parameters: [forall params, Ui] *) mind_arity_ctxt : rel_context; @@ -616,7 +616,7 @@ type one_inductive_body = { mind_arity : inductive_arity; (* Names of the constructors: [cij] *) - mind_consnames : identifier array; + mind_consnames : Id.t array; (* Types of the constructors with parameters: [forall params, Tij], where the Ik are replaced by de Bruijn index in the context @@ -764,8 +764,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 = { mod_mp : module_path; |