diff options
Diffstat (limited to 'test-suite')
| -rwxr-xr-x | test-suite/coq-makefile/timing/run.sh | 2 | ||||
| -rw-r--r-- | test-suite/output/bug5778.out | 4 | ||||
| -rw-r--r-- | test-suite/output/bug6404.out | 4 | ||||
| -rw-r--r-- | test-suite/output/bug6404.v | 7 |
4 files changed, 14 insertions, 3 deletions
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index aa6b0a9a43..43c83e412a 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -40,7 +40,7 @@ INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected TO_SED_IN_BOTH=( -e s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" # Whether or not something shows up as ∞ depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent - -e s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent + -e s':|\s*N/A\s*$:| '"${INFINITY_REPLACEMENT}"':g' # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent -e s'/ *$//g' # the number of trailing spaces depends on how many digits percentages end up being; since this varies across runs, we remove trailing spaces -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out index 91ceb1b583..d6056c5098 100644 --- a/test-suite/output/bug5778.out +++ b/test-suite/output/bug5778.out @@ -1,4 +1,4 @@ The command has indeed failed with message: -In nested Ltac calls to "c", "abs" and "abstract b ltac:(())", last call -failed. +In nested Ltac calls to "c", "abs", "abstract b ltac:(())", +"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed. The term "I" has type "True" which should be Set, Prop or Type. diff --git a/test-suite/output/bug6404.out b/test-suite/output/bug6404.out new file mode 100644 index 0000000000..05464755f0 --- /dev/null +++ b/test-suite/output/bug6404.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +In nested Ltac calls to "c", "abs", "transparent_abstract (tactic3)", +"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed. +The term "I" has type "True" which should be Set, Prop or Type. diff --git a/test-suite/output/bug6404.v b/test-suite/output/bug6404.v new file mode 100644 index 0000000000..bbe6b1a00f --- /dev/null +++ b/test-suite/output/bug6404.v @@ -0,0 +1,7 @@ +Ltac a _ := pose (I : I). +Ltac b _ := a (). +Ltac abs _ := transparent_abstract b (). +Ltac c _ := abs (). +Goal True. + Fail c (). +Abort. |