From c3318ad8408b1ceb0bfd4c2bfedec63ce9324698 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 Jun 2018 14:59:15 +0200 Subject: Change the proj_ind field from MutInd.t to inductive. This is a first step towards the acceptance of mutual record types in the kernel. --- pretyping/detyping.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index fe49d64c7..23a985dc3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -690,8 +690,7 @@ and detype_r d flags avoid env sigma t = let c' = try let pb = Environ.lookup_projection p (snd env) in - (** FIXME: handle mutual records *) - let ind = (pb.Declarations.proj_ind, 0) in + let ind = pb.Declarations.proj_ind 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 -- cgit v1.2.3