Merge PR #10489: Fix output for "Printing Dependent Evars Line"

Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: hendriktews
Reviewed-by: herbelin
Ack-by: mattam82

4 files changed, 262 insertions, 0 deletions

diff --git a/test-suite/output-coqtop/DependentEvars.out b/test-suite/output-coqtop/DependentEvars.out
new file mode 100644
index 0000000000..9ca3fa3357
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars.out
@@ -0,0 +1,91 @@
+
+Coq < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+strange_imp_trans < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q : Prop, (P -> Q) /\ P -> Q
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+modpon < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+Coq < Coq < 
+Coq < P1 is declared
+P2 is declared
+P3 is declared
+P4 is declared
+
+Coq < p12 is declared
+
+Coq < p123 is declared
+
+Coq < p34 is declared
+
+Coq < Coq < 1 subgoal
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  P4
+
+(dependent evars: ; in current goal:)
+
+p14 < 
+p14 < 4 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?Q -> P4
+
+subgoal 2 is:
+ ?P -> ?Q
+subgoal 3 is:
+ ?P -> ?Q
+subgoal 4 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < 3 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?P -> (?Goal2 -> P4) /\ ?Goal2
+
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
+
+p14 < 
+Coq < 
+Coq < 
diff --git a/test-suite/output-coqtop/DependentEvars.v b/test-suite/output-coqtop/DependentEvars.v
new file mode 100644
index 0000000000..5a59054073
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars.v
@@ -0,0 +1,24 @@
+Set Printing Dependent Evars Line.
+Lemma strange_imp_trans :
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R.
+Proof.
+  auto.
+Qed.
+
+Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q.
+Proof.
+  tauto.
+Qed.
+
+Section eex.
+  Variables P1 P2 P3 P4 : Prop.
+  Hypothesis p12 : P1 -> P2.
+  Hypothesis p123 : (P1 -> P2) -> P3.
+  Hypothesis p34 : P3 -> P4.
+
+  Lemma p14 : P4.
+  Proof.
+    eapply strange_imp_trans.
+          apply modpon.
+  Abort.
+End eex.
diff --git a/test-suite/output-coqtop/DependentEvars2.out b/test-suite/output-coqtop/DependentEvars2.out
new file mode 100644
index 0000000000..29ebba7c86
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars2.out
@@ -0,0 +1,120 @@
+
+Coq < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+strange_imp_trans < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q : Prop, (P -> Q) /\ P -> Q
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+modpon < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+Coq < Coq < 
+Coq < P1 is declared
+P2 is declared
+P3 is declared
+P4 is declared
+
+Coq < p12 is declared
+
+Coq < p123 is declared
+
+Coq < p34 is declared
+
+Coq < Coq < 1 subgoal
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  P4
+
+(dependent evars: ; in current goal:)
+
+p14 < 
+p14 < Second proof:
+
+p14 < 4 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?Q -> P4
+
+subgoal 2 is:
+ ?P -> ?Q
+subgoal 3 is:
+ ?P -> ?Q
+subgoal 4 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < 1 focused subgoal
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?Q -> P4
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < This subproof is complete, but there are some unfocused goals.
+Try unfocusing with "}".
+
+3 subgoals
+(shelved: 2)
+
+subgoal 1 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal:)
+
+p14 < 3 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?P -> (?Goal2 -> P4) /\ ?Goal2
+
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
+
+p14 < 
+Coq < 
+Coq < 
diff --git a/test-suite/output-coqtop/DependentEvars2.v b/test-suite/output-coqtop/DependentEvars2.v
new file mode 100644
index 0000000000..d0f3a4012e
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars2.v
@@ -0,0 +1,27 @@
+Set Printing Dependent Evars Line.
+Lemma strange_imp_trans :
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R.
+Proof.
+  auto.
+Qed.
+
+Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q.
+Proof.
+  tauto.
+Qed.
+
+Section eex.
+  Variables P1 P2 P3 P4 : Prop.
+  Hypothesis p12 : P1 -> P2.
+  Hypothesis p123 : (P1 -> P2) -> P3.
+  Hypothesis p34 : P3 -> P4.
+
+  Lemma p14 : P4.
+  Proof.
+    idtac "Second proof:".
+    eapply strange_imp_trans.
+          {
+            apply modpon.
+          }
+  Abort.
+End eex.