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, 1 insertions, 7 deletions

diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 970f3e2abd..4f20f1649c 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -47,12 +47,6 @@ val new_class : identifier located ->
   local_binder list ->
   binder_list -> unit
 
-(* By default, print the free variables that are implicitely generalized. *)
-
-val default_on_free_vars : identifier list -> unit
-
-val fail_on_free_vars : identifier list -> unit
-
 (* Instance declaration *)
 
 val declare_instance : bool -> identifier located -> unit
@@ -73,7 +67,7 @@ val new_instance :
   local_binder list ->
   typeclass_constraint ->
   binder_def_list ->
-  ?on_free_vars:(identifier list -> unit) ->
+  ?generalize:bool ->
   ?tac:Proof_type.tactic  ->
   ?hook:(constant -> unit) ->
   int option ->