diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-05 14:59:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-23 01:38:33 +0200 |
| commit | c3318ad8408b1ceb0bfd4c2bfedec63ce9324698 (patch) | |
| tree | ac38feed833aaa28038e0144109f34305fc44cc8 /pretyping | |
| parent | f337d237c97db0b29619e15d21a022bba953a794 (diff) | |
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.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 3 |
1 files changed, 1 insertions, 2 deletions
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 |