diff options
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | test-suite/output/NumeralNotations.out | 4 | ||||
| -rw-r--r-- | test-suite/output/NumeralNotations.v | 15 | ||||
| -rw-r--r-- | test-suite/success/NumeralNotationsNoLocal.v | 12 |
4 files changed, 13 insertions, 20 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a8e7ef8fd4..ec3702b360 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -365,7 +365,7 @@ pkg:nix:deploy:channel: - echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null - git fetch --unshallow - git branch -v - - git push git@github.com:coq/coq-on-cachix "${CI_COMMIT_SHA}":"${CI_COMMIT_REF_NAME}" + - git push git@github.com:coq/coq-on-cachix "${CI_COMMIT_SHA}":"refs/heads/${CI_COMMIT_REF_NAME}" pkg:nix: extends: .nix-template diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out index cb49e66ed7..460c77879c 100644 --- a/test-suite/output/NumeralNotations.out +++ b/test-suite/output/NumeralNotations.out @@ -82,10 +82,6 @@ function (of_uint) targets an option type. The command has indeed failed with message: The 'abstract after' directive has no effect when the parsing function (of_uint) targets an option type. [abstract-large-number-no-op,numbers] -The command has indeed failed with message: -The reference of_uint was not found in the current environment. -The command has indeed failed with message: -The reference of_uint was not found in the current environment. let v := of_uint (Decimal.D1 Decimal.Nil) in v : unit : unit let v := 0%test13 in v : unit diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v index fcfdd82dcc..44805ad09d 100644 --- a/test-suite/output/NumeralNotations.v +++ b/test-suite/output/NumeralNotations.v @@ -207,21 +207,6 @@ Module Test10. Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1). End Test10. -Module Test11. - (* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *) - Inductive unit11 := tt11. - Declare Scope unit11_scope. - Delimit Scope unit11_scope with unit11. - Goal True. - evar (to_uint : unit11 -> Decimal.uint). - evar (of_uint : Decimal.uint -> unit11). - Fail Numeral Notation unit11 of_uint to_uint : uint11_scope. - exact I. - Unshelve. - all: solve [ constructor ]. - Qed. -End Test11. - Module Test12. (* Test for numeral notations on context variables *) Declare Scope test12_scope. diff --git a/test-suite/success/NumeralNotationsNoLocal.v b/test-suite/success/NumeralNotationsNoLocal.v new file mode 100644 index 0000000000..ea3907ef8a --- /dev/null +++ b/test-suite/success/NumeralNotationsNoLocal.v @@ -0,0 +1,12 @@ +(* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *) +Inductive unit11 := tt11. +Declare Scope unit11_scope. +Delimit Scope unit11_scope with unit11. +Goal True. + evar (to_uint : unit11 -> Decimal.uint). + evar (of_uint : Decimal.uint -> unit11). + Fail Numeral Notation unit11 of_uint to_uint : uint11_scope. + exact I. + Unshelve. + all: solve [ constructor ]. +Qed. |