diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-29 10:21:59 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-29 12:46:54 +0200 |
commit | 9501ddd635adea7db07b4df60b8bda1d557dff18 (patch) | |
tree | 8bfed1a20bc8e2c3e27711a0a80fd6ff337d3634 /test-suite/bugs/closed/4865.v | |
parent | 4965fa03bd9cbc37dd6888c7d13c3fba83b2652c (diff) |
Fixing #4865 (deciding on which arguments to recompute scopes was not robust).
See 4865.v for details.
Diffstat (limited to 'test-suite/bugs/closed/4865.v')
-rw-r--r-- | test-suite/bugs/closed/4865.v | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4865.v b/test-suite/bugs/closed/4865.v new file mode 100644 index 000000000..c5bf3289b --- /dev/null +++ b/test-suite/bugs/closed/4865.v @@ -0,0 +1,52 @@ +(* Check discharge of arguments scopes + other checks *) + +(* This is bug #4865 *) + +Notation "<T>" := true : bool_scope. +Section A. + Check negb <T>. + Global Arguments negb : clear scopes. + Fail Check negb <T>. +End A. + +(* Check that no scope is re-computed *) +Fail Check negb <T>. + +(* Another test about arguments scopes in sections *) + +Notation "0" := true. +Section B. + Variable x : nat. + Let T := nat -> nat. + Definition f y : T := fun z => x + y + z. + Fail Check f 1 0. (* 0 in nat, 0 in bool *) + Fail Check f 0 0. (* 0 in nat, 0 in bool *) + Check f 0 1. (* 0 and 1 in nat *) + Global Arguments f _%nat_scope _%nat_scope. + Check f 0 0. (* both 0 in nat *) +End B. + +(* Check that only the scope for the extra product on x is re-computed *) +Check f 0 0 0. (* All 0 in nat *) + +Section C. + Variable x : nat. + Let T := nat -> nat. + Definition g y : T := fun z => x + y + z. + Global Arguments g : clear scopes. + Check g 1. (* 1 in nat *) +End C. + +(* Check that only the scope for the extra product on x is re-computed *) +Check g 0. (* 0 in nat *) +Fail Check g 0 1 0. (* 2nd 0 in bool *) +Fail Check g 0 0 1. (* 2nd 0 in bool *) + +(* Another test on arguments scopes: checking scope for expanding arities *) +(* Not sure this is very useful, but why not *) + +Fixpoint arr n := match n with 0%nat => nat | S n => nat -> arr n end. +Fixpoint lam n : arr n := match n with 0%nat => 0%nat | S n => fun x => lam n end. +Notation "0" := true. +Arguments Scope lam [nat_scope nat_scope]. +Check (lam 1 0). |