diff options
| author | Pierre-Marie Pédrot | 2016-11-20 20:09:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:34 +0100 |
| commit | d4b344acb23f19b089098b7788f37ea22bc07b81 (patch) | |
| tree | 6dd26d747b259793ef6a24befd27e13234b19875 /pretyping/inductiveops.mli | |
| parent | 2cd0648e003308a000f9f89c898bce4d15fc94a1 (diff) | |
Eliminating parts of the right-hand side compatibility layer
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 1614e1817e..4bb4847591 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -161,9 +161,9 @@ val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) -val extract_mrectype : evar_map -> EConstr.t -> pinductive * constr list -val find_mrectype : env -> evar_map -> EConstr.types -> pinductive * constr list -val find_mrectype_vect : env -> evar_map -> EConstr.types -> pinductive * constr array +val extract_mrectype : evar_map -> EConstr.t -> pinductive * EConstr.constr list +val find_mrectype : env -> evar_map -> EConstr.types -> pinductive * EConstr.constr list +val find_mrectype_vect : env -> evar_map -> EConstr.types -> pinductive * EConstr.constr array val find_rectype : env -> evar_map -> EConstr.types -> inductive_type val find_inductive : env -> evar_map -> EConstr.types -> pinductive * constr list val find_coinductive : env -> evar_map -> EConstr.types -> pinductive * constr list |