From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- test-suite/bugs/closed/4865.v | 52 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) create mode 100644 test-suite/bugs/closed/4865.v (limited to 'test-suite/bugs/closed/4865.v') diff --git a/test-suite/bugs/closed/4865.v b/test-suite/bugs/closed/4865.v new file mode 100644 index 00000000..c5bf3289 --- /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 "" := true : bool_scope. +Section A. + Check negb . + Global Arguments negb : clear scopes. + Fail Check negb . +End A. + +(* Check that no scope is re-computed *) +Fail Check negb . + +(* 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). -- cgit v1.2.3