diff options
| author | Hugo Herbelin | 2020-08-22 18:58:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-25 15:36:47 +0200 |
| commit | 27c1b6504b04c7653eced708492626be28a4f868 (patch) | |
| tree | a21f2dcd425ea6903231b31b21d85acea583270c | |
| parent | 7f82d1387860860f1f6b2fb6e01759e92274349f (diff) | |
The body of a let is considered to be "in context" if its type is present.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
| -rw-r--r-- | interp/constrextern.ml | 2 | ||||
| -rw-r--r-- | test-suite/output/Implicit.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Implicit.v | 10 |
3 files changed, 15 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8a29fc3581..43fef8685d 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1000,7 +1000,7 @@ let rec extern inctx ?impargs scopes vars r = mkFlattenedCApp (head,args)) | GLetIn (na,b,t,c) -> - CLetIn (make ?loc na,sub_extern false scopes vars b, + CLetIn (make ?loc na,sub_extern (Option.has_some t) scopes vars b, Option.map (extern_typ scopes vars) t, extern inctx ?impargs scopes (add_vname vars na) c) diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 2265028d3e..d8b88b8c1c 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -17,3 +17,7 @@ fix f (x : nat) : option nat := match x with | S _ => x end : nat -> option nat +fun x : False => let y := False_rect (A:=bool) x in y + : False -> bool +fun x : False => let y : True := False_rect x in y + : False -> True diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index a7c4399e38..86420bd8c8 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -61,3 +61,13 @@ Coercion some_nat := @Some nat. Check fix f x := match x with 0 => None | n => some_nat n end. End MatchBranchesInContext. + +Module LetInContext. + +Set Implicit Arguments. +Set Contextual Implicit. +Axiom False_rect : forall A:Type, False -> A. +Check fun x:False => let y:= False_rect (A:=bool) x in y. (* will not be in context: explicitation *) +Check fun x:False => let y:= False_rect (A:=True) x in y. (* will be in context: no explicitation *) + +End LetInContext. |