From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 test-suite/success/AdvancedCanonicalStructure.v | 27 ++++++++++++-------------
 1 file changed, 13 insertions(+), 14 deletions(-)

(limited to 'test-suite/success/AdvancedCanonicalStructure.v')

diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v
index 8e613dca..b533db6e 100644
--- a/test-suite/success/AdvancedCanonicalStructure.v
+++ b/test-suite/success/AdvancedCanonicalStructure.v
@@ -21,7 +21,6 @@ Parameter eq_img : forall (i1:img) (i2:img),
   eqB (ib i1) (ib i2) -> eqA (ia i1) (ia i2).
 
 Lemma phi_img (a:A) : img.
-  intro a.
   exists  a (phi a).
   refine ( refl_equal _).
 Defined.
@@ -54,7 +53,7 @@ Open Scope type_scope.
 
 Section type_reification.
 
-Inductive term :Type := 
+Inductive term :Type :=
    Fun : term -> term -> term
  | Prod : term -> term -> term
  | Bool : term
@@ -63,18 +62,18 @@ Inductive term :Type :=
  | TYPE :term
  | Var : Type -> term.
 
-Fixpoint interp (t:term) := 
-  match t with 
+Fixpoint interp (t:term) :=
+  match t with
     Bool => bool
   | SET => Set
   | PROP => Prop
-  | TYPE => Type   
+  | TYPE => Type
   | Fun a b => interp a -> interp b
   | Prod a b => interp a * interp b
   | Var x => x
 end.
 
-Record interp_pair :Type := 
+Record interp_pair :Type :=
   { repr:>term;
     abs:>Type;
     link: abs = interp repr }.
@@ -95,25 +94,25 @@ thus thesis using rewrite (link a);rewrite (link b);reflexivity.
 end proof.
 Qed.
 
-Canonical Structure ProdCan (a b:interp_pair) := 
+Canonical Structure ProdCan (a b:interp_pair) :=
   Build_interp_pair (Prod a b) (a * b) (prod_interp a b).
 
-Canonical Structure FunCan (a b:interp_pair) := 
+Canonical Structure FunCan (a b:interp_pair) :=
   Build_interp_pair (Fun a b) (a -> b) (fun_interp a b).
 
-Canonical Structure BoolCan := 
+Canonical Structure BoolCan :=
   Build_interp_pair Bool bool (refl_equal _).
 
-Canonical Structure VarCan (x:Type) := 
+Canonical Structure VarCan (x:Type) :=
   Build_interp_pair (Var x) x (refl_equal _).
 
-Canonical Structure SetCan := 
+Canonical Structure SetCan :=
   Build_interp_pair SET Set (refl_equal _).
 
-Canonical Structure PropCan := 
+Canonical Structure PropCan :=
   Build_interp_pair PROP Prop (refl_equal _).
 
-Canonical Structure TypeCan := 
+Canonical Structure TypeCan :=
   Build_interp_pair TYPE Type (refl_equal _).
 
 (* Print Canonical Projections. *)
@@ -140,5 +139,5 @@ End type_reification.
 
 
 
- 
+
 
-- 
cgit v1.2.3