From 0c3ffbbacec5e61d0d7bbeb8c25ec33ce429f40d Mon Sep 17 00:00:00 2001
From: glondu
Date: Tue, 5 Oct 2010 16:50:24 +0000
Subject: test-suite: fix success/AdvancedCanonicalStructure.v

I have no idea how this test could have ever worked... (ssreflect?
declarative mode?)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13501 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/AdvancedCanonicalStructure.v | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v
index b533db6eac..97cf316cad 100644
--- a/test-suite/success/AdvancedCanonicalStructure.v
+++ b/test-suite/success/AdvancedCanonicalStructure.v
@@ -79,19 +79,17 @@ Record interp_pair :Type :=
     link: abs = interp repr }.
 
 Lemma prod_interp :forall (a b:interp_pair),a * b = interp (Prod a b) .
-proof.
-let a:interp_pair,b:interp_pair.
-reconsider thesis as (a * b = interp a * interp b).
-thus thesis by (link a),(link b).
-end proof.
+Proof.
+intros a b.
+change (a * b = interp a * interp b).
+rewrite (link a), (link b); reflexivity.
 Qed.
 
 Lemma fun_interp :forall (a b:interp_pair), (a -> b) = interp (Fun a b).
-proof.
-let a:interp_pair,b:interp_pair.
-reconsider thesis as ((a -> b) = (interp a -> interp b)).
-thus thesis using rewrite (link a);rewrite (link b);reflexivity.
-end proof.
+Proof.
+intros a b.
+change ((a -> b) = (interp a -> interp b)).
+rewrite (link a), (link b); reflexivity.
 Qed.
 
 Canonical Structure ProdCan (a b:interp_pair) :=
-- 
cgit v1.2.3