Implicit_quantifiers
val declare_generalizable : local:bool -> Names.lident list option -> unit
Fragile, should be used only for construction a set of identifiers to avoid
val free_vars_of_constr_expr :
Constrexpr.constr_expr ->
?bound:Names.Id.Set.t ->
Names.Id.t list ->
Names.Id.t list
Returns the generalizable free ids in left-to-right order with the location of their first occurrence
val generalizable_vars_of_glob_constr :
?bound:Names.Id.Set.t ->
?allowed:Names.Id.Set.t ->
Glob_term.glob_constr ->
Names.lident list
val make_fresh : Names.Id.Set.t -> Environ.env -> Names.Id.t -> Names.Id.t
val implicits_of_glob_constr :
?with_products:bool ->
Glob_term.glob_constr ->
Impargs.manual_implicits
val implicit_application :
Names.Id.Set.t ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr * Names.Id.Set.t