Generalized implementation of generalization.

- New constr_expr construct [CGeneralization of loc * binding_kind *
abstraction_kind option * constr_expr] to generalize the free vars of
the [constr_expr], binding these using [binding_kind] and making
a lambda or a pi (or deciding from the scope) using [abstraction_kind
option] (abstraction_kind = AbsLambda | AbsPi)
- Concrete syntax "`( a = 0 )" for explicit binding of [a] and "`{
... }" for implicit bindings (both "..(" and "_(" seem much more
difficult to implement). Subject to discussion! A few examples added
in a test-suite file.
- Also add missing syntax for implicit/explicit combinations for
_binders_: "{( )}" means implicit for the generalized (outer) vars,
explicit for the (inner) variable itself. Subject to discussion as well :)
- Factor much typeclass instance declaration code. We now just have to
force generalization of the term after the : in instance declarations.
One more step to using Instance for records.


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

1 files changed, 2 insertions, 11 deletions

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index b58998d1f..d286b190f 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -93,21 +93,12 @@ Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A)
    : Irreflexive (complement R).
 
   Next Obligation. 
-  Proof. 
-    unfold complement.
-    red. intros H.
-    intros H' ; apply H'.
-    apply reflexivity.
-  Qed.
-
+  Proof. firstorder. Qed.
 
 Program Instance complement_Symmetric [ Symmetric A (R : relation A) ] : Symmetric (complement R).
 
   Next Obligation.
-  Proof.
-    red ; intros H'.
-    apply (H (symmetry H')).
-  Qed.
+  Proof. firstorder. Qed.
 
 (** * Standard instances. *)