diff options
| author | Maxime Dénès | 2018-06-29 14:30:33 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-29 14:30:33 +0200 |
| commit | 2ca003899ea4a24a470c32dc186b95ef3de3ca19 (patch) | |
| tree | e7444295b47223d16db6db5beafde4839a0cf926 /pretyping/inductiveops.mli | |
| parent | acbc42ad1da48be53456c0d41ec2e60ae2d6e642 (diff) | |
| parent | 21ed95122a088cab6808200778719270d9cc9078 (diff) | |
Merge PR #7080: Swapping Context and Constr and defining declarations on constr in Constr
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index aa53f7e67c..8eaef24c48 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -93,12 +93,12 @@ val inductive_nparamdecls : inductive -> int val inductive_nparamdecls_env : env -> inductive -> int (** @return params context *) -val inductive_paramdecls : pinductive -> Context.Rel.t -val inductive_paramdecls_env : env -> pinductive -> Context.Rel.t +val inductive_paramdecls : pinductive -> Constr.rel_context +val inductive_paramdecls_env : env -> pinductive -> Constr.rel_context (** @return full arity context, hence with letin *) -val inductive_alldecls : pinductive -> Context.Rel.t -val inductive_alldecls_env : env -> pinductive -> Context.Rel.t +val inductive_alldecls : pinductive -> Constr.rel_context +val inductive_alldecls_env : env -> pinductive -> Constr.rel_context (** {7 Extract information from a constructor name} *) @@ -141,7 +141,7 @@ 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 : Context.Rel.t; (* signature of the arguments (letin included) *) + cs_args : Constr.rel_context; (* 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 @@ -154,7 +154,7 @@ val get_projections : env -> inductive_family -> Constant.t 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 -> Context.Rel.t * Sorts.family +val get_arity : env -> inductive_family -> Constr.rel_context * Sorts.family val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr |