diff options
| author | Gaëtan Gilbert | 2019-02-22 22:59:47 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-22 22:59:47 +0100 |
| commit | c37e90b67c74b32837409a9a424757246067ef1b (patch) | |
| tree | 639db4ec57048e96a50a9711c9d15f7c72fe9346 | |
| parent | dea9f08178efcf9cfac7ee2970dc21abc2fde308 (diff) | |
| parent | c5e2f573ef079800eed4c8246c4f2bd39bf47b26 (diff) | |
Merge PR #9364: Apply implicit binders to Hypothesis inside sections.
Reviewed-by: SkySkimmer
| -rw-r--r-- | CHANGES.md | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_9363.v | 17 | ||||
| -rw-r--r-- | test-suite/success/AdvancedTypeClasses.v | 2 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 1 |
4 files changed, 21 insertions, 1 deletions
diff --git a/CHANGES.md b/CHANGES.md index c309002beb..af2b7991dd 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -135,6 +135,8 @@ Vernacular commands - The algorithm computing implicit arguments now behaves uniformly for primitive projection and application nodes (bug #9508). +- `Hypotheses` and `Variables` can now take implicit binders inside sections. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: diff --git a/test-suite/bugs/closed/bug_9363.v b/test-suite/bugs/closed/bug_9363.v new file mode 100644 index 0000000000..a3f6ad9fa2 --- /dev/null +++ b/test-suite/bugs/closed/bug_9363.v @@ -0,0 +1,17 @@ +(* Outside a section, Hypothesis, Variable, Axiom all obey implicit binders *) +Hypothesis foo1 : forall {n : nat}, True. +Variable foo1' : forall {n : nat}, True. +Axiom foo1'' : forall {n : nat}, True. +Check foo1 (n := 1). +Check foo1' (n := 1). +Check foo1'' (n := 1). + +Section bar. +(* Inside a section, Hypothesis and Variable do not, but they should *) +Hypothesis foo2 : forall {n : nat}, True. +Variable foo2' : forall {n : nat}, True. +Axiom foo2'' : forall {n : nat}, True. +Check foo2 (n := 1). +Check foo2' (n := 1). +Check foo2'' (n := 1). +End bar. diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v index d0aa5c8578..0253ec46e4 100644 --- a/test-suite/success/AdvancedTypeClasses.v +++ b/test-suite/success/AdvancedTypeClasses.v @@ -71,7 +71,7 @@ Variable Inhabited: term -> Prop. Variable Inhabited_correct: forall `{interp_pair p}, Inhabited (repr p) -> p. Lemma L : Prop * A -> bool * (Type -> Set) . -apply (Inhabited_correct _ _). +apply Inhabited_correct. change (Inhabited (Fun (Prod PROP (Var A)) (Prod Bool (Fun TYPE SET)))). Admitted. diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 4fb06e4e09..35d8be5c56 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -57,6 +57,7 @@ match local with strbrk " is not visible from current goals") in let r = VarRef ident in + let () = maybe_declare_manual_implicits true r imps in let () = Typeclasses.declare_instance None true r in let () = if is_coe then Class.try_add_new_coercion r ~local:true false in (r,Univ.Instance.empty,true) |