diff options
| author | Maxime Dénès | 2017-07-28 18:25:30 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-28 18:25:30 +0200 |
| commit | 17f37f42792b3150fcebb6236b9896845957b89d (patch) | |
| tree | 5e76522bd7e5b16fe37907386f589a290078f0a0 /test-suite | |
| parent | e8bb8ea0da02b926e076cf04ea1c82c547a30ea2 (diff) | |
| parent | df49e6b29fa9e8ac971c3e08f20ae6cb0f5b9889 (diff) | |
Merge PR #923: [api] Fix base_include LTAC parts.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/TypeclassDebug.out | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out index 73369ab713..8b38fe0ff4 100644 --- a/test-suite/output/TypeclassDebug.out +++ b/test-suite/output/TypeclassDebug.out @@ -1,18 +1,18 @@ Debug: 1: looking for foo without backtracking Debug: 1.1: simple apply H on foo, 1 subgoal(s) -Debug: 1.1-2 : foo -Debug: 1.1-2: looking for foo without backtracking -Debug: 1.1-2.1: simple apply H on foo, 1 subgoal(s) -Debug: 1.1-2.1-2 : foo -Debug: 1.1-2.1-2: looking for foo without backtracking -Debug: 1.1-2.1-2.1: simple apply H on foo, 1 subgoal(s) -Debug: 1.1-2.1-2.1-2 : foo -Debug: 1.1-2.1-2.1-2: looking for foo without backtracking -Debug: 1.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s) -Debug: 1.1-2.1-2.1-2.1-2 : foo -Debug: 1.1-2.1-2.1-2.1-2: looking for foo without backtracking -Debug: 1.1-2.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s) -Debug: 1.1-2.1-2.1-2.1-2.1-2 : foo +Debug: 1.1-1 : foo +Debug: 1.1-1: looking for foo without backtracking +Debug: 1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1 : foo +Debug: 1.1-1.1-1: looking for foo without backtracking +Debug: 1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1.1-1 : foo +Debug: 1.1-1.1-1.1-1: looking for foo without backtracking +Debug: 1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1.1-1.1-1 : foo +Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking +Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo The command has indeed failed with message: Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed. Tactic failure: Proof search reached its limit. |