diff options
| author | Hugo Herbelin | 2019-02-18 19:02:23 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-02-18 19:02:23 +0100 |
| commit | ee6d8274483711f84277e449494c3a11a64dfea8 (patch) | |
| tree | fad80601c725129060f5da8d88c79c82814dc454 /test-suite/output/FunExt.out | |
| parent | 1dbb4e77051324e229f7006161746030e5369565 (diff) | |
| parent | b1e0fa29b62ee958b31c55ea3c8eea4087e6e2b4 (diff) | |
Merge PR #9142: Disable Ltac backtraces
Ack-by: Zimmi48
Reviewed-by: jfehrle
Ack-by: ppedrot
Diffstat (limited to 'test-suite/output/FunExt.out')
| -rw-r--r-- | test-suite/output/FunExt.out | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out index 8d2a125c1d..2a823396d5 100644 --- a/test-suite/output/FunExt.out +++ b/test-suite/output/FunExt.out @@ -1,19 +1,12 @@ The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Not an extensional equality. The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Not an extensional equality. The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Not an extensional equality. The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Not an extensional equality. The command has indeed failed with message: -Ltac call to "extensionality in (var)" failed. Tactic failure: Already an intensional equality. The command has indeed failed with message: -In nested Ltac calls to "extensionality in (var)" and -"clearbody (ne_var_list)", last call failed. Hypothesis e depends on the body of H' |