diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-29 14:32:25 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-29 14:57:12 +0200 |
| commit | 449123ef56e7d323d89ba2cc331b007f695b29e9 (patch) | |
| tree | a63c481a850cb48f1a121e8b2089614aee0cf069 /pretyping/tacred.ml | |
| parent | 883611696f3388ac5fb9b08930f0ea4564749446 (diff) | |
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.
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 |