diff options
| author |  Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
| commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
| tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /interp/implicit_quantifiers.mli | |
| parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
| parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) | |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'interp/implicit_quantifiers.mli')
| -rw-r--r-- | interp/implicit_quantifiers.mli | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 4442e09d..5a13bfd1 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: implicit_quantifiers.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Decl_kinds open Term @@ -17,12 +14,11 @@ open Evd open Environ open Nametab open Mod_subst -open Rawterm +open Glob_term open Topconstr open Util open Libnames open Typeclasses -(*i*) val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit @@ -30,7 +26,7 @@ val ids_of_list : identifier list -> Idset.t val destClassApp : constr_expr -> loc * reference * constr_expr list val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list -(* Fragile, should be used only for construction a set of identifiers to avoid *) +(** Fragile, should be used only for construction a set of identifiers to avoid *) val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t -> identifier list -> identifier list @@ -38,15 +34,15 @@ val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t -> val free_vars_of_binders : ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list -(* Returns the generalizable free ids in left-to-right +(** Returns the generalizable free ids in left-to-right order with the location of their first occurence *) -val generalizable_vars_of_rawconstr : ?bound:Idset.t -> ?allowed:Idset.t -> - rawconstr -> (Names.identifier * loc) list +val generalizable_vars_of_glob_constr : ?bound:Idset.t -> ?allowed:Idset.t -> + glob_constr -> (Names.identifier * loc) list val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier -val implicits_of_rawterm : ?with_products:bool -> Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list +val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits val combine_params_freevar : Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) -> |