diff options
| -rw-r--r-- | pretyping/cbv.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4634.v | 16 |
2 files changed, 17 insertions, 1 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 43062a0e8..afd86420e 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -310,7 +310,7 @@ and cbv_stack_value info env = function | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk))) when red_set (info_flags info) fIOTA && Projection.unfolded p -> let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in - cbv_stack_value info env (arg, stk) + cbv_stack_value info env (strip_appl arg stk) (* may be reduced later by application *) | (FIXP(fix,env,[||]), APP(appl,TOP)) -> FIXP(fix,env,appl) diff --git a/test-suite/bugs/closed/4634.v b/test-suite/bugs/closed/4634.v new file mode 100644 index 000000000..77e31e108 --- /dev/null +++ b/test-suite/bugs/closed/4634.v @@ -0,0 +1,16 @@ +Set Primitive Projections. + +Polymorphic Record pair {A B : Type} : Type := + prod { pr1 : A; pr2 : B }. + +Notation " ( x ; y ) " := (@prod _ _ x y). +Notation " x .1 " := (pr1 x) (at level 3). +Notation " x .2 " := (pr2 x) (at level 3). + +Goal ((0; 1); 2).1.2 = 1. +Proof. + cbv. + match goal with + | |- ?t = ?t => exact (eq_refl t) + end. +Qed. |