Fixes in the documentation of [dependent induction] and test-suite

scripts.


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

1 files changed, 8 insertions, 7 deletions

diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v
index b4535b3ba..e6950a2a1 100644
--- a/test-suite/success/AdvancedTypeClasses.v
+++ b/test-suite/success/AdvancedTypeClasses.v
@@ -47,17 +47,18 @@ Lemma fun_interp' :forall `{ia : interp_pair, ib : interp_pair}, (ia -> ib) = in
 Qed.
 
 Instance ProdCan `(interp_pair a, interp_pair b) : interp_pair (a * b) :=
-  repr := Prod (repr a) (repr b) ; link := prod_interp.
+  { repr := Prod (repr a) (repr b) ; link := prod_interp }.
 
 Instance FunCan `(interp_pair a, interp_pair b) : interp_pair (a -> b) :=
-  link := fun_interp.
+  { link := fun_interp }.
 
-Instance BoolCan : interp_pair bool := repr := Bool ; link := refl_equal _.
+Instance BoolCan : interp_pair bool := 
+  { repr := Bool ; link := refl_equal _ }.
 
-Instance VarCan : interp_pair x | 10 := repr := Var x ; link := refl_equal _.
-Instance SetCan : interp_pair Set := repr := SET ; link := refl_equal _.
-Instance PropCan : interp_pair Prop := repr := PROP ; link := refl_equal _.
-Instance TypeCan : interp_pair Type := repr := TYPE ; link := refl_equal _.
+Instance VarCan : interp_pair x | 10 := { repr := Var x ; link := refl_equal _ }.
+Instance SetCan : interp_pair Set := { repr := SET ; link := refl_equal _ }.
+Instance PropCan : interp_pair Prop := { repr := PROP ; link := refl_equal _ }.
+Instance TypeCan : interp_pair Type := { repr := TYPE ; link := refl_equal _ }.
 
 (* Print Canonical Projections. *)