From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/ideal-features/Case9.v | 2 +- test-suite/ideal-features/complexity/evars_subst.v | 6 +++--- test-suite/ideal-features/eapply_evar.v | 4 ++-- test-suite/ideal-features/evars_subst.v | 6 +++--- test-suite/ideal-features/implicit_binders.v | 22 +++++++++++----------- test-suite/ideal-features/universes.v | 4 ++-- 6 files changed, 22 insertions(+), 22 deletions(-) (limited to 'test-suite/ideal-features') diff --git a/test-suite/ideal-features/Case9.v b/test-suite/ideal-features/Case9.v index 800c431ec..d95c21084 100644 --- a/test-suite/ideal-features/Case9.v +++ b/test-suite/ideal-features/Case9.v @@ -6,7 +6,7 @@ CoInductive hdlist : unit -> Type := Variable P : forall bo, hdlist bo -> Prop. Variable all : forall bo l, P bo l. -Definition F (l:hdlist tt) : P tt l := +Definition F (l:hdlist tt) : P tt l := match l in hdlist u return P u l with | cons (cons l') => all tt _ end. diff --git a/test-suite/ideal-features/complexity/evars_subst.v b/test-suite/ideal-features/complexity/evars_subst.v index 6f9f86a95..b3dfb33cd 100644 --- a/test-suite/ideal-features/complexity/evars_subst.v +++ b/test-suite/ideal-features/complexity/evars_subst.v @@ -3,12 +3,12 @@ (* Let n be the number of let-in. The complexity comes from the fact that each implicit arguments of f was in a larger and larger - context. To compute the type of "let _ := f ?Tn 0 in f ?T 0", + context. To compute the type of "let _ := f ?Tn 0 in f ?T 0", "f ?Tn 0" is substituted in the type of "f ?T 0" which is ?T. This type is an evar instantiated on the n variables denoting the "f ?Ti 0". One obtain "?T[1;...;n-1;f ?Tn[1;...;n-1] 0]". To compute the type of "let _ := f ?Tn-1 0 in let _ := f ?Tn 0 in f ?T 0", another - substitution is done leading to + substitution is done leading to "?T[1;...;n-2;f ?Tn[1;...;n-2] 0;f ?Tn[1;...;n-2;f ?Tn[1;...;n-2] 0] 0]" and so on. At the end, we get a term of exponential size *) @@ -25,7 +25,7 @@ Time Check let _ := f _ 0 in let _ := f _ 0 in let _ := f _ 0 in - + let _ := f _ 0 in let _ := f _ 0 in let _ := f _ 0 in diff --git a/test-suite/ideal-features/eapply_evar.v b/test-suite/ideal-features/eapply_evar.v index b10d5dbf9..8c9a448e7 100644 --- a/test-suite/ideal-features/eapply_evar.v +++ b/test-suite/ideal-features/eapply_evar.v @@ -1,9 +1,9 @@ (* Test propagation of evars from subgoal to brother subgoals *) -(* This does not work (oct 2008) because "match goal" sees "?evar = O" +(* This does not work (oct 2008) because "match goal" sees "?evar = O" and not "O = O" Lemma eapply_evar : O=O -> 0=O. -intro H; eapply trans_equal; +intro H; eapply trans_equal; [apply H | match goal with |- ?x = ?x => reflexivity end]. Qed. diff --git a/test-suite/ideal-features/evars_subst.v b/test-suite/ideal-features/evars_subst.v index 6f9f86a95..b3dfb33cd 100644 --- a/test-suite/ideal-features/evars_subst.v +++ b/test-suite/ideal-features/evars_subst.v @@ -3,12 +3,12 @@ (* Let n be the number of let-in. The complexity comes from the fact that each implicit arguments of f was in a larger and larger - context. To compute the type of "let _ := f ?Tn 0 in f ?T 0", + context. To compute the type of "let _ := f ?Tn 0 in f ?T 0", "f ?Tn 0" is substituted in the type of "f ?T 0" which is ?T. This type is an evar instantiated on the n variables denoting the "f ?Ti 0". One obtain "?T[1;...;n-1;f ?Tn[1;...;n-1] 0]". To compute the type of "let _ := f ?Tn-1 0 in let _ := f ?Tn 0 in f ?T 0", another - substitution is done leading to + substitution is done leading to "?T[1;...;n-2;f ?Tn[1;...;n-2] 0;f ?Tn[1;...;n-2;f ?Tn[1;...;n-2] 0] 0]" and so on. At the end, we get a term of exponential size *) @@ -25,7 +25,7 @@ Time Check let _ := f _ 0 in let _ := f _ 0 in let _ := f _ 0 in - + let _ := f _ 0 in let _ := f _ 0 in let _ := f _ 0 in diff --git a/test-suite/ideal-features/implicit_binders.v b/test-suite/ideal-features/implicit_binders.v index 5b66944b5..2ec727808 100644 --- a/test-suite/ideal-features/implicit_binders.v +++ b/test-suite/ideal-features/implicit_binders.v @@ -1,8 +1,8 @@ (** * Questions de syntaxe autour de la généralisation implicite ** Lieurs de classes - Aujourd'hui, les lieurs de classe [ ] et les - lieurs {{ }} sont équivalents et on a toutes les combinaisons de { et ( pour + Aujourd'hui, les lieurs de classe [ ] et les + lieurs {{ }} sont équivalents et on a toutes les combinaisons de { et ( pour les lieurs de classes (où la variable liée peut être anonyme): *) @@ -22,7 +22,7 @@ Definition bar₄ {( F : Foo A )} (x y : A) := foo x + foo y. (** Les lieurs sont généralisés à tous les termes, pas seulement aux classes: *) -Definition relation A := A -> A -> Prop. +Definition relation A := A -> A -> Prop. Definition inverse {( R : relation A )} := fun x y => R y x. @@ -43,7 +43,7 @@ Definition inverse {( R : relation A )} := fun x y => R y x. [Definition inverse _{R : relation A} := fun x y => R y x] [Definition inverse `(R : relation A) := fun x y => R y x] et - + [Definition inverse `[R : relation A] := fun x y => R y x] ou [Definition inverse `{R : relation A} := fun x y => R y x] @@ -53,7 +53,7 @@ Definition inverse {( R : relation A )} := fun x y => R y x. Definition div (x : nat) ({ y <> 0 }) := 0. -(** Un choix à faire pour les inductifs: accepter ou non de ne pas donner de nom à +(** Un choix à faire pour les inductifs: accepter ou non de ne pas donner de nom à l'argument. Manque de variables anonymes pour l'utilisateur mais pas pour le système... *) Inductive bla [ Foo A ] : Type :=. @@ -73,10 +73,10 @@ Definition instimpl ({ SomeStruct a }) : nat := a + a. (** Donne l'instance explicitement (façon foncteur). *) -Definition foo_prod {( Foo A, Foo B )} : Foo (A * B) := +Definition foo_prod {( Foo A, Foo B )} : Foo (A * B) := fun x => let (l, r) := x in foo l + foo r. -(** *** Questions: +(** *** Questions: - Gardez les crochets [ ] pour {{ }} ? - Quelle syntaxe pour la généralisation ? - Veut-on toutes les combinaisons de statut pour les variables généralisées et la variable liée ? @@ -98,12 +98,12 @@ Definition baz := `{x + y + z = x + (y + z)}. Print baz. (** Proposition d'Arthur C.: déclarer les noms de variables généralisables à la [Implicit Types] - pour plus de robustesse (cela vaudrait aussi pour les lieurs). Les typos du genre de l'exemple suivant + pour plus de robustesse (cela vaudrait aussi pour les lieurs). Les typos du genre de l'exemple suivant ne sont plus silencieuses: *) Check `(foob 0 + x). -(** Utilisé pour généraliser l'implémentation de la généralisation implicite dans +(** Utilisé pour généraliser l'implémentation de la généralisation implicite dans les déclarations d'instances (i.e. les deux defs suivantes sont équivalentes). *) Instance fooa : Foo A. @@ -111,8 +111,8 @@ Admitted. Definition fooa' : `(Foo A). Admitted. -(** Un peu différent de la généralisation des lieurs qui "explosent" les variables - libres en les liant au même niveau que l'objet. Dans la deuxième defs [a] n'est pas lié dans +(** Un peu différent de la généralisation des lieurs qui "explosent" les variables + libres en les liant au même niveau que l'objet. Dans la deuxième defs [a] n'est pas lié dans la définition mais [F : Π a, SomeStruct a]. *) Definition qux {( F : SomeStruct a )} : nat := a. diff --git a/test-suite/ideal-features/universes.v b/test-suite/ideal-features/universes.v index 6db4cfe18..49530ebce 100644 --- a/test-suite/ideal-features/universes.v +++ b/test-suite/ideal-features/universes.v @@ -7,7 +7,7 @@ Definition Ty := Type (* Top.1 *). Inductive Q (A:Type (* Top.2 *)) : Prop := q : A -> Q A. Inductive T (B:Type (* Top.3 *)) := t : B -> Q (T B) -> T B. -(* ajoute Top.4 <= Top.2 inutilement: +(* ajoute Top.4 <= Top.2 inutilement: 4 est l'univers utilisé dans le calcul du type polymorphe de T *) Definition C := T Ty. (* ajoute Top.1 < Top.3 : @@ -23,7 +23,7 @@ Definition C := T Ty. Definition f (A:Type (* Top.1 *)) := True. Inductive R := r : f R -> R. -(* ajoute Top.3 <= Top.1 inutilement: +(* ajoute Top.3 <= Top.1 inutilement: Top.3 est l'univers utilisé dans le calcul du type polymorphe de R *) (* mais il manque la contrainte que l'univers de R est plus petit que Top.1 -- cgit v1.2.3