diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-07 15:20:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-24 18:03:56 +0100 |
| commit | 1161ccf74578c3190d296dc37f39edecf28cf078 (patch) | |
| tree | 852666e60de305821eb94cdeadb1923f45b87fed /test-suite/output | |
| parent | e59d58b6db222332f7d7ad2adcb2b78c24fb351e (diff) | |
Printing again "intros **" as "intros" by default.
The rationale it that it is more common to do so and thus more
"natural" (principle of writing less whenever possible).
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/ltac.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 7f3cdad6c..eb9f57102 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,7 +1,7 @@ The command has indeed failed with message: Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := - symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize + symmetry in x, y; auto with z; auto; intros; clearbody x; generalize dependent z The command has indeed failed with message: In nested Ltac calls to "g1" and "refine (uconstr)", last call failed. |