diff options
| -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. |