diff options
| -rw-r--r-- | CHANGES.md | 2 | ||||
| -rw-r--r-- | Makefile.build | 8 | ||||
| -rwxr-xr-x | dev/build/windows/MakeCoq_MinGW.bat | 2 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_4509.v | 11 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_6202.v | 11 | ||||
| -rw-r--r-- | test-suite/output/Arguments.v | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 8 |
8 files changed, 34 insertions, 12 deletions
diff --git a/CHANGES.md b/CHANGES.md index 8cb71f19ea..4fafb9a18a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -88,6 +88,8 @@ Vernacular commands - The `Automatic Introduction` option has been removed and is now the default. +- `Arguments` now accepts names for arguments provided with `extra_scopes`. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: diff --git a/Makefile.build b/Makefile.build index 0a73562467..34d7ce42f7 100644 --- a/Makefile.build +++ b/Makefile.build @@ -575,11 +575,11 @@ module Gramext = Gramlib__Gramext \ module Grammar = Gramlib__Grammar" > $@ gramlib/.pack/gramlib__P%: gramlib/p% | gramlib/.pack - cp -a $< $@ - sed -e "1i # 1 \"$<\"" -i $@ + printf '# 1 "%s"\n' $< > $@ + cat $< >> $@ gramlib/.pack/gramlib__G%: gramlib/g% | gramlib/.pack - cp -a $< $@ - sed -e "1i # 1 \"$<\"" -i $@ + printf '# 1 "%s"\n' $< > $@ + cat $< >> $@ # Specific rules for gramlib to pack it Dune / OCaml 4.08 style GRAMOBJS=$(addsuffix .cmo, $(GRAMFILES)) diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 33feeed45c..8489bcfc3a 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -55,7 +55,7 @@ IF DEFINED HTTP_PROXY ( )
REM see -cygrepo in ReadMe.txt
-SET CYGWIN_REPOSITORY=http://ftp.inf.tu-dresden.de/software/windows/cygwin32
+SET CYGWIN_REPOSITORY=http://mirror.easyname.at/cygwin
REM see -cygcache in ReadMe.txt
SET CYGWIN_LOCAL_CACHE_WFMT=%BATCHDIR%cygwin_cache
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index a54da6faf2..47afa5ba0c 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -70,7 +70,7 @@ associativity rules have to be given. The right-hand side of a notation is interpreted at the time the notation is given. In particular, disambiguation of constants, :ref:`implicit arguments - <ImplicitArguments>`, :ref:`coercions <Coercions>`, etc. are resolved at the + <ImplicitArguments>` and other notations are resolved at the time of the declaration of the notation. Precedences and associativity diff --git a/test-suite/bugs/closed/bug_4509.v b/test-suite/bugs/closed/bug_4509.v new file mode 100644 index 0000000000..ceae7c5fc3 --- /dev/null +++ b/test-suite/bugs/closed/bug_4509.v @@ -0,0 +1,11 @@ +(* Was solved at some time, suspectingly in PR #6328 *) + +Goal exists n, n > 1. +Proof. + unshelve eexists. (*2 goals, as expected*) + Undo. + unshelve (eexists; instantiate (1:=ltac:(idtac))). (*only 1 goal*) + shelve. + Undo. + 2:unshelve instantiate (1:=_). +Abort. diff --git a/test-suite/bugs/closed/bug_6202.v b/test-suite/bugs/closed/bug_6202.v new file mode 100644 index 0000000000..899260f59a --- /dev/null +++ b/test-suite/bugs/closed/bug_6202.v @@ -0,0 +1,11 @@ +(* This was fixed at some time, suspectingly in PR #6328 *) + +Inductive foo := F (a : forall var : Type -> Type, unit -> var unit) (_ : a = a). +Goal foo. + eexists (fun var => fun u : unit => ltac:(clear u)). + shelve. + Unshelve. + all:[ > | ]. + shelve. + Fail Grab Existential Variables. +Abort. diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index 97df40f882..844f96aaa1 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -51,7 +51,7 @@ Arguments pi _ _%F _%B. Check (forall w : r, pi w $ $ = tt). Fail Check (forall w : r, w $ $ = tt). Axiom w : r. -Arguments w _%F _%B : extra scopes. +Arguments w x%F y%B : extra scopes. Check (w $ $ = tt). Fail Arguments w _%F _%B. diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3fa3681661..c6c6f74152 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1221,11 +1221,9 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red let rec check_extra_args extra_args = match extra_args with | [] -> () - | { notation_scope = None } :: _ -> err_extra_args (names_of extra_args) - | { name = Anonymous; notation_scope = Some _ } :: args -> - check_extra_args args - | _ -> - user_err Pp.(str "Extra notation scopes can be set on anonymous and explicit arguments only.") + | { notation_scope = None } :: _ -> + user_err Pp.(str"Extra arguments should specify a scope.") + | { notation_scope = Some _ } :: args -> check_extra_args args in let args, scopes = |