From 449123ef56e7d323d89ba2cc331b007f695b29e9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 29 Jul 2014 14:32:25 +0200 Subject: Rework code for refolding projections in whd_state/whd_simpl to allow Arguments Specifications indicating that the record object must be a constructor. Fixes bug #3432. --- pretyping/tacred.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'pretyping/tacred.ml') diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 7b26a73b1..fad8623b0 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -738,7 +738,9 @@ and whd_simpl_stack env sigma = (match ReductionBehaviour.get (ConstRef p) with | Some (l, n, f) when List.mem `ReductionNeverUnfold f -> (* simpl never *) s' | Some (l, n, f) when not (List.is_empty l) -> - let l' = List.map (fun i -> i - (pb.Declarations.proj_npars + 1)) l in + let l' = List.map_filter (fun i -> + let idx = (i - (pb.Declarations.proj_npars + 1)) in + if idx < 0 then None else Some idx) l in let stack = reduce_params env sigma stack l' in (match reduce_projection env sigma pb (whd_construct_stack env sigma c) stack -- cgit v1.2.3