diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 4ad32fc66..1a790be64 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -549,6 +549,9 @@ let compute_projections env (kn, _ as ind) = in Array.rev_of_list pbs +let legacy_match_projection env ind = + Array.map pi3 (compute_projections env ind) + let compute_projections ind mib = let ans = compute_projections ind mib in Array.map (fun (prj, ty, _) -> (prj, ty)) ans |