diff options
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 4 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 24 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12390.v | 3 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 2 |
4 files changed, 28 insertions, 5 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index ba552ab302..4a6555a4f7 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1880,9 +1880,9 @@ function make_addon_quickchick { # Flocq: Floating point library function make_addon_flocq { - if build_prep_overlay Flocq; then + if build_prep_overlay flocq; then installer_addon_section flocq "Flocq" "Coq library for floating point arithmetic" "" - logn autogen ./autogen.sh + log1 autoconf logn configure ./configure logn remake ./remake --jobs=$MAKE_THREADS logn install ./remake install diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index b0bbbf33b3..aec3607349 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -923,12 +923,32 @@ class CoqtopBlocksTransform(Transform): @staticmethod def split_lines(source): - """Split Coq input in chunks + r"""Split Coq input in chunks A chunk is a minimal sequence of consecutive lines of the input that ends with a '.' + + >>> split_lines('A.\nB.''') + ['A.', 'B.'] + + >>> split_lines('A.\n\nB.''') + ['A.', '\nB.'] + + >>> split_lines('A.\n\nB.\n''') + ['A.', '\nB.'] + + >>> split_lines("SearchPattern (_ + _ = _ + _).\n" + ... "SearchPattern (nat -> bool).\n" + ... "SearchPattern (forall l : list _, _ l l).") + ... # doctest: +NORMALIZE_WHITESPACE + ['SearchPattern (_ + _ = _ + _).', + 'SearchPattern (nat -> bool).', + 'SearchPattern (forall l : list _, _ l l).'] + + >>> split_lines('SearchHead le.\nSearchHead (@eq bool).') + ['SearchHead le.', 'SearchHead (@eq bool).'] """ - return re.split(r"(?<=(?<!\.)\.)\s+\n", source) + return re.split(r"(?<=(?<!\.)\.)\n", source.strip()) @staticmethod def parse_options(node): diff --git a/test-suite/bugs/closed/bug_12390.v b/test-suite/bugs/closed/bug_12390.v new file mode 100644 index 0000000000..a8fda29a6f --- /dev/null +++ b/test-suite/bugs/closed/bug_12390.v @@ -0,0 +1,3 @@ +Fail Inductive foo : forall P, P := . +Fail Inductive bar : nat := . +Fail Inductive baz : _ := . diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 4242f06844..95489c9132 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -117,7 +117,7 @@ let intern_ind_arity env sigma ind = let pretype_ind_arity env sigma (loc, c, impls, pseudo_poly) = let sigma,t = understand_tcc env sigma ~expected_type:IsType c in match Reductionops.sort_of_arity env sigma t with - | exception Invalid_argument _ -> + | exception Reduction.NotArity -> user_err ?loc (str "Not an arity") | s -> let concl = match pseudo_poly with |