diff options
| author | Hugo Herbelin | 2020-05-31 18:38:34 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-06-01 19:56:12 +0200 |
| commit | f12b5b295afcd387624a8404a1385f5a1a66e2a9 (patch) | |
| tree | 1f47ce205c5a659694426fe6a055d59ed3fcca1a /test-suite/output-coqtop/DependentEvars.out | |
| parent | a1fa186fc8314e395a0813bb23c2c73d738b7572 (diff) | |
Slight improvement in naming existential variables.
In a Meta := Evar unification problem and the Meta is bound to a
(named) binder, and the Evar is a GoalEvar, we set the source of the
evar to be the one of the Meta.
Diffstat (limited to 'test-suite/output-coqtop/DependentEvars.out')
| -rw-r--r-- | test-suite/output-coqtop/DependentEvars.out | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/output-coqtop/DependentEvars.out b/test-suite/output-coqtop/DependentEvars.out index 9ca3fa3357..2e69b94505 100644 --- a/test-suite/output-coqtop/DependentEvars.out +++ b/test-suite/output-coqtop/DependentEvars.out @@ -77,14 +77,14 @@ p14 < 3 focused subgoals p123 : (P1 -> P2) -> P3 p34 : P3 -> P4 ============================ - ?P -> (?Goal2 -> P4) /\ ?Goal2 + ?P -> (?P0 -> P4) /\ ?P0 subgoal 2 is: - ?P -> (?Goal2 -> P4) /\ ?Goal2 + ?P -> (?P0 -> P4) /\ ?P0 subgoal 3 is: ?P -(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11) +(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal: ?X4 ?X5 ?X10 ?X11) p14 < Coq < |