(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* Names.Id.Set.t -> Names.Id.Set.t (* [minimize_unused_hyps e s1] gives [s2] s.t. [Id.Set.subset s2 s1] is [true] * and s.t. calling [clear s1] would do the same as [clear s2]. Inefficient. *) val minimize_unused_hyps : Environ.env -> Names.Id.Set.t -> Names.Id.Set.t val process_expr : Environ.env -> Vernacexpr.section_subset_descr -> Constr.types list -> Names.Id.t list val name_set : Names.Id.t -> Vernacexpr.section_subset_descr -> unit val to_string : Vernacexpr.section_subset_descr -> string val get_default_proof_using : unit -> string option