Bypassing the use of (currently unimplemented) "Show Script" in tests

that used it.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14802 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 16 insertions, 30 deletions

diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index c69d31f401..a13ae4624a 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -9,17 +9,4 @@ let fix f (m : nat) : nat := match m with
                              | S m' => f m'
                              end in f 0
      : nat
-fix even_pos_odd_pos 2
- with (odd_pos_even_pos (n:_) (H:odd n) {struct H} : n >= 1).
- intros.
- destruct H.
-  omega.
-  
-  apply odd_pos_even_pos in H.
-  omega.
-  
- intros.
- destruct H.
- apply even_pos_odd_pos in H.
- omega.
- 
+Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1)
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index af5f05f653..8afa50ba57 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -25,6 +25,11 @@ Inductive even: Z -> Prop :=
 with odd: Z -> Prop :=
 | odd_succ: forall n, even (n - 1) -> odd n.
 
+(* Check printing of fix *)
+Ltac f id1 id2 := fix id1 2 with (id2 n (H:odd n) {struct H} : n >= 1).
+Print Ltac f.
+
+(* Incidentally check use of fix in proofs *)
 Lemma even_pos_odd_pos: forall n, even n -> n >= 0.
 Proof.
 fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
@@ -37,5 +42,6 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
  destruct H.
   apply even_pos_odd_pos in H.
   omega.
-Show Script.
 Qed.
+
+
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index ac5eedc175..9949658c44 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1,6 +1,4 @@
-intro H; split; [ a H | e H ].
-
-intros; match goal with
-        | |- context [if ?X then _ else _] => case X
-        end; trivial.
-
+Ltac f H := split; [ a H | e H ]
+Ltac g := match goal with
+          | |- context [if ?X then _ else _] => case X
+          end
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index 8fa9199408..a7c497cfaf 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -3,16 +3,11 @@
 Tactic Notation "a" constr(x) := apply x.
 Tactic Notation "e" constr(x) := exact x.
 
-Lemma test : True -> True /\ True.
-intro H; split; [a H|e H].
-Show Script.
-Qed.
+Ltac f H := split; [a H|e H].
+Print Ltac f.
 
 (* Test printing of match context *)
 (* Used to fail after translator removal (see bug #1070) *)
 
-Lemma test2 : forall n:nat, forall f: nat -> bool, O = if (f n) then O else O.
-Proof.
-intros;match goal with |- context [if ?X then _ else _ ] => case X end;trivial.
-Show Script.
-Qed.
+Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end.
+Print Ltac g.