diff options
| -rw-r--r-- | pretyping/patternops.ml | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5486.v | 15 |
2 files changed, 17 insertions, 2 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 75d3ed30b..79e9c727d 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -360,9 +360,9 @@ let rec pat_of_raw metas vars = function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (loc,nal,(_,None),b,c) -> - let mkGLambda c na = + let mkGLambda na c = GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, IntroAnonymous, None),c) in - let c = List.fold_left mkGLambda c nal in + let c = List.fold_right mkGLambda nal c in let cip = { cip_style = LetStyle; cip_ind = None; diff --git a/test-suite/bugs/closed/5486.v b/test-suite/bugs/closed/5486.v new file mode 100644 index 000000000..390133162 --- /dev/null +++ b/test-suite/bugs/closed/5486.v @@ -0,0 +1,15 @@ +Axiom proof_admitted : False. +Tactic Notation "admit" := abstract case proof_admitted. +Goal forall (T : Type) (p : prod (prod T T) bool) (Fm : Set) (f : Fm) (k : + forall _ : T, Fm), + @eq Fm + (k + match p return T with + | pair p0 swap => fst p0 + end) f. + intros. + (* next statement failed in Bug 5486 *) + match goal with + | [ |- ?f (let (a, b) := ?d in @?e a b) = ?rhs ] + => pose (let (a, b) := d in e a b) as t0 + end. |