diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 16:34:24 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 20:41:04 +0200 |
| commit | 0f17c70288662bf8abd1bae59d32a94054481f26 (patch) | |
| tree | f604cd6de5f1274b3e54dcfe48bc84cf0494d473 /pretyping/retyping.ml | |
| parent | 84544396cbbf34848be2240acf181b4d5f1f42d2 (diff) | |
Make pattern_of_constr typed so that we can infer the proper patterns
for primitive projections, fixing bug #3661. Also fix expand_projection
so that it does enough reduction to find the inductive type of its
argument.
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index b16cf75f5..89ad9ee68 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -244,6 +244,6 @@ let sorts_of_context env evc ctxt = let expand_projection env sigma pr c args = let ty = get_type_of env sigma c in - let (i,u), ind_args = Inductive.find_rectype env ty in + let (i,u), ind_args = Inductiveops.find_mrectype env sigma ty in mkApp (mkConstU (Projection.constant pr,u), Array.of_list (ind_args @ (c :: args))) |