diff options
| author | Jasper Hugunin | 2019-05-19 01:38:59 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2019-05-19 01:38:59 -0700 |
| commit | d8d665f900ee92fac8f776031a9a6a0981a4ed2e (patch) | |
| tree | fd73e59456e3b290dbad1a9e970d0e9ab2cd3b01 | |
| parent | d61c293eb0fc99eb921ef5ea599bbab8ac7aedcc (diff) | |
Implicit Quantifiers recurse in continuation of let-in
| -rw-r--r-- | interp/implicit_quantifiers.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_10189.v | 9 |
2 files changed, 10 insertions, 1 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index dffccf02fc..6277d874dd 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -281,7 +281,7 @@ let implicits_of_glob_constr ?(with_products=true) l = | _ -> () in [] | GLambda (na, bk, t, b) -> abs na bk b - | GLetIn (na, b, t, c) -> aux i b + | GLetIn (na, b, t, c) -> aux i c | GRec (fix_kind, nas, args, tys, bds) -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) diff --git a/test-suite/bugs/closed/bug_10189.v b/test-suite/bugs/closed/bug_10189.v new file mode 100644 index 0000000000..d603bff386 --- /dev/null +++ b/test-suite/bugs/closed/bug_10189.v @@ -0,0 +1,9 @@ +Definition foo : forall (x := unit) {y : nat}, nat := fun y => y. +Check foo (y := 3). (*We fail to get implicits in the type past a let-in*) +Definition foo' : forall (x : Set) {y : nat}, nat := fun _ y => y. +Check foo' unit (y := 3). (* It works with a function binder *) + +Definition bar := let f {x} : nat -> nat := fun y => x in f (x := 3). +(* Adding bar : nat -> nat gives implicits-in-term warning *) +Fail Check bar (x := 3). +(* The implicits from the type of the local definition leak to the outer term *) |