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, 6 insertions, 8 deletions

diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 744b45272f..5934272091 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -43,13 +43,11 @@ val free_vars_of_binders :
 
 val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
 
-val combine_params : Names.Idset.t ->
+val combine_params_freevar :
+  Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
+  Topconstr.constr_expr * Names.Idset.t
+
+val implicit_application : Idset.t -> ?allow_partial:bool ->
   (Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
     Topconstr.constr_expr * Names.Idset.t) ->
-  (Topconstr.constr_expr * Topconstr.explicitation located option) list ->
-  ((global_reference * bool) option * Term.rel_declaration) list ->
-  Topconstr.constr_expr list * Names.Idset.t
-
-val full_class_binder : Idset.t -> 
-  loc * reference * (constr_expr * explicitation located option) list ->
-  global_reference -> constr_expr
+  constr_expr -> constr_expr