diff options
| author | Matthieu Sozeau | 2014-09-27 16:08:02 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-27 20:41:04 +0200 |
| commit | 84544396cbbf34848be2240acf181b4d5f1f42d2 (patch) | |
| tree | 72d398f334bdc7b1c6a0ee333a05940c34780f12 /pretyping/detyping.ml | |
| parent | 0efba04058ba28889c83553224309be216873298 (diff) | |
Add a boolean to indicate the unfolding state of a primitive projection,
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 07540af57b..0b0ff2fb59 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -445,12 +445,22 @@ let rec detype flags avoid env sigma t = | Proj (p,c) -> if fst flags || !Flags.in_debugger || !Flags.in_toplevel then (* lax mode, used by debug printers only *) - GApp (dl, GRef (dl, ConstRef p, None), + GApp (dl, GRef (dl, ConstRef (Projection.constant p), None), [detype flags avoid env sigma c]) - else let ty = Retyping.get_type_of (snd env) sigma c in - let (ind, args) = Inductive.find_rectype (snd env) ty in - GApp (dl, GRef (dl, ConstRef p, None), - List.map (detype flags avoid env sigma) (args @ [c])) + else + if Projection.unfolded p then + (** Print the compatibility match version *) + let pb = Environ.lookup_projection p (snd env) in + let body = pb.Declarations.proj_body in + let ty = Retyping.get_type_of (snd env) sigma c in + let (ind, args) = Inductive.find_rectype (snd env) ty in + let body' = strip_lam_assum body in + detype flags avoid env sigma (substl (c :: List.rev args) body') + else + let ty = Retyping.get_type_of (snd env) sigma c in + let (ind, args) = Inductive.find_rectype (snd env) ty in + GApp (dl, GRef (dl, ConstRef (Projection.constant p), None), + List.map (detype flags avoid env sigma) (args @ [c])) | Evar (evk,cl) -> let id,l = try Evd.evar_ident evk sigma, |