diff options
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index b2e205115f..5a4257e175 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -194,14 +194,6 @@ val compute_projections : Environ.env -> inductive -> (constr * types) array (** Given a primitive record type, for every field computes the eta-expanded projection and its type. *) -val legacy_match_projection : Environ.env -> inductive -> constr array -(** Given a record type, computes the legacy match-based projection of the - projections. - - BEWARE: such terms are ill-typed, and should thus only be used in upper - layers. The kernel will probably badly fail if presented with one of - those. *) - (********************) val type_of_inductive_knowing_conclusion : |