diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 5 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 3 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 8 |
3 files changed, 15 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index df89d9eac..5a54c6f05 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -690,7 +690,10 @@ and detype_r d flags avoid env sigma t = let c' = try let pb = Environ.lookup_projection p (snd env) in - let body = pb.Declarations.proj_body in + (** FIXME: handle mutual records *) + let ind = (pb.Declarations.proj_ind, 0) in + let bodies = Inductiveops.legacy_match_projection (snd env) ind in + let body = bodies.(pb.Declarations.proj_arg) in let ty = Retyping.get_type_of (snd env) sigma c in let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in let body' = strip_lam_assum body in 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 diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 506cdd8c9..aa53f7e67 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -198,6 +198,14 @@ 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 : |