From 0f17c70288662bf8abd1bae59d32a94054481f26 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 27 Sep 2014 16:34:24 +0200 Subject: 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. --- pretyping/retyping.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/retyping.ml') 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))) -- cgit v1.2.3