From 57cb1648fcf7da18d74c28a4d63d59ea129ab136 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 23 Oct 2008 12:49:34 +0000
Subject: 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
---
 interp/implicit_quantifiers.mli | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

(limited to 'interp/implicit_quantifiers.mli')

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
-- 
cgit v1.2.3