Imported Upstream snapshot 8.3~beta0+13298

7 files changed, 142 insertions, 38 deletions

diff --git a/test-suite/ideal-features/Case3.v b/test-suite/ideal-features/Case3.v
deleted file mode 100644
index de7784ae..00000000
--- a/test-suite/ideal-features/Case3.v
+++ /dev/null
@@ -1,29 +0,0 @@
-Inductive Le : nat -> nat -> Set :=
-  | LeO : forall n : nat, Le 0 n
-  | LeS : forall n m : nat, Le n m -> Le (S n) (S m).
-
-Parameter discr_l : forall n : nat, S n <> 0.
-
-Type
-  (fun n : nat =>
-   match n return (n = 0 \/ n <> 0) with
-   | O => or_introl (0 <> 0) (refl_equal 0)
-   | S O => or_intror (1 = 0) (discr_l 0)
-   | S (S x) => or_intror (S (S x) = 0) (discr_l (S x))
-   end).
-
-Parameter iguales : forall (n m : nat) (h : Le n m), Prop.
-
-Type
-  match LeO 0 as h in (Le n m) return Prop with
-  | LeO O => True
-  | LeS (S x) (S y) H => iguales (S x) (S y) H
-  | _ => False
-  end.
-
-Type
-  match LeO 0 as h in (Le n m) return Prop with
-  | LeO O => True
-  | LeS (S x) O H => iguales (S x) 0 H
-  | _ => False
-  end.
diff --git a/test-suite/ideal-features/Case9.v b/test-suite/ideal-features/Case9.v
index 800c431e..d95c2108 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 6f9f86a9..b3dfb33c 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
new file mode 100644
index 00000000..547860bf
--- /dev/null
+++ b/test-suite/ideal-features/eapply_evar.v
@@ -0,0 +1,9 @@
+(* Test propagation of evars from subgoal to brother subgoals *)
+
+(* 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;
+  [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 6f9f86a9..b3dfb33c 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
new file mode 100644
index 00000000..2ec72780
--- /dev/null
+++ b/test-suite/ideal-features/implicit_binders.v
@@ -0,0 +1,124 @@
+(** * 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
+   les lieurs de classes (où la variable liée peut être anonyme):
+   *)
+
+Class Foo (A : Type) := foo : A -> nat.
+
+Definition bar [ Foo A ] (x y : A) := foo x + foo y.
+
+Definition bar₀ {{ Foo A }} (x y : A) := foo x + foo y.
+
+Definition bar₁ {( Foo A )} (x y : A) := foo x + foo y.
+
+Definition bar₂ ({ Foo A }) (x y : A) := foo x + foo y.
+
+Definition bar₃ (( Foo A )) (x y : A) := foo x + foo y.
+
+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 inverse {( R : relation A )} := fun x y => R y x.
+
+(** Autres propositions:
+   [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]
+   pour lier [R] implicitement.
+
+   MS: Le .. empêche d'utiliser electric-terminator dans Proof General. Cependant, il existe
+   aussi les caractères utf8 ‥ (two dot leader) et … (horizontal ellipsis) qui permettraient
+   d'éviter ce souci moyennant l'utilisation d'unicode.
+
+   [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]
+
+   [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]
+
+
+   Toujours avec la possibilité de ne pas donner le nom de la variable:
+*)
+
+Definition div (x : nat) ({ y <> 0 }) := 0.
+
+(** 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 :=.
+
+(** *** Les autres syntaxes ne supportent pas de pouvoir spécifier séparément les statuts
+   des variables généralisées et celui de la variable liée. Ca peut être utile pour les
+   classes où l'on a les cas de figure: *)
+
+(** Trouve [A] et l'instance par unification du type de [x]. *)
+Definition allimpl {{ Foo A }} (x : A) : A := x.
+
+(** Trouve l'instance à partir de l'index explicite *)
+
+Class SomeStruct (a : nat) := non_zero : a <> 0.
+
+Definition instimpl ({ SomeStruct a }) : nat := a + a.
+
+(** Donne l'instance explicitement (façon foncteur). *)
+
+Definition foo_prod {( Foo A, Foo B )} : Foo (A * B) :=
+  fun x => let (l, r) := x in foo l + foo r.
+
+(** *** 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 ?
+   *)
+
+(** ** Constructeur de généralisation implicite
+
+   Permet de faire une généralisation n'importe où dans le terme: on
+   utilise un produit ou un lambda suivant le scope (fragile ?).
+   *)
+
+Goal `(x + y + z = x + (y + z)).
+Admitted.
+
+(** La généralisation donne un statut implicite aux variables si l'on utilise
+   `{ }. *)
+
+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
+   ne sont plus silencieuses: *)
+
+Check `(foob 0 + x).
+
+(** 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.
+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
+   la définition mais [F : Π a, SomeStruct a]. *)
+
+Definition qux {( F : SomeStruct a )} : nat := a.
+Definition qux₁ {( F : `(SomeStruct a) )} : nat := 0.
+
+(** *** Questions
+   - Autres propositions de syntaxe ?
+   - Réactions sur la construction ?
+   *)
\ No newline at end of file
diff --git a/test-suite/ideal-features/universes.v b/test-suite/ideal-features/universes.v
index 6db4cfe1..49530ebc 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