From 67f5c70a480c95cfb819fc68439781b5e5e95794 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Dec 2012 15:56:25 +0000 Subject: Modulification of identifier git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/declarations.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'checker/declarations.mli') diff --git a/checker/declarations.mli b/checker/declarations.mli index 7dfe609c3..c14d8b73a 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -91,7 +91,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; @@ -100,7 +100,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 @@ -191,8 +191,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; -- cgit v1.2.3