From f22ad605a14eb14d11b0a1615f7014f2dca3b483 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Nov 2015 17:38:18 +0100 Subject: An example in centralizing similar functions to a common place so that cleaning the interfaces is eventually easier. Here, adding find_mrectype_vect to simplify vnorm.ml. --- pretyping/inductiveops.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'pretyping/inductiveops.mli') diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 757599a3ce..9036f521ec 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -159,6 +159,7 @@ val build_branch_type : env -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) val extract_mrectype : constr -> pinductive * constr list val find_mrectype : env -> evar_map -> types -> pinductive * constr list +val find_mrectype_vect : env -> evar_map -> types -> pinductive * constr array val find_rectype : env -> evar_map -> types -> inductive_type val find_inductive : env -> evar_map -> types -> pinductive * constr list val find_coinductive : env -> evar_map -> types -> pinductive * constr list -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- pretyping/inductiveops.mli | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) (limited to 'pretyping/inductiveops.mli') diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 9036f521ec..42a00a7e22 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Declarations open Environ open Evd @@ -92,12 +91,12 @@ val inductive_nparamdecls : inductive -> int val inductive_nparamdecls_env : env -> inductive -> int (** @return params context *) -val inductive_paramdecls : pinductive -> rel_context -val inductive_paramdecls_env : env -> pinductive -> rel_context +val inductive_paramdecls : pinductive -> Context.Rel.t +val inductive_paramdecls_env : env -> pinductive -> Context.Rel.t (** @return full arity context, hence with letin *) -val inductive_alldecls : pinductive -> rel_context -val inductive_alldecls_env : env -> pinductive -> rel_context +val inductive_alldecls : pinductive -> Context.Rel.t +val inductive_alldecls_env : env -> pinductive -> Context.Rel.t (** {7 Extract information from a constructor name} *) @@ -133,9 +132,9 @@ val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> type constructor_summary = { cs_cstr : pconstructor; (* internal name of the constructor plus universes *) - cs_params : constr list; (* parameters of the constructor in current ctx *) - cs_nargs : int; (* length of arguments signature (letin included) *) - cs_args : rel_context; (* signature of the arguments (letin included) *) + cs_params : constr list; (* parameters of the constructor in current ctx *) + cs_nargs : int; (* length of arguments signature (letin included) *) + cs_args : Context.Rel.t; (* signature of the arguments (letin included) *) cs_concl_realargs : constr array; (* actual realargs in the concl of cstr *) } val lift_constructor : int -> constructor_summary -> constructor_summary @@ -148,11 +147,11 @@ val get_projections : env -> inductive_family -> constant array option (** [get_arity] returns the arity of the inductive family instantiated with the parameters; if recursively non-uniform parameters are not part of the inductive family, they appears in the arity *) -val get_arity : env -> inductive_family -> rel_context * sorts_family +val get_arity : env -> inductive_family -> Context.Rel.t * sorts_family val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr -val make_arity_signature : env -> bool -> inductive_family -> rel_context +val make_arity_signature : env -> bool -> inductive_family -> Context.Rel.t val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- pretyping/inductiveops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/inductiveops.mli') diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 757599a3ce..7cd2ff2af5 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*