package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val or_var_map : ('a -> 'b) -> 'a Locus.or_var -> 'b Locus.or_var
val occurrences_map : ('a list -> 'b list) -> 'a Locus.occurrences_gen -> 'b Locus.occurrences_gen
val convert_occs : Locus.occurrences -> bool * int list
val is_selected : int -> Locus.occurrences -> bool
val is_all_occurrences : 'a Locus.occurrences_gen -> bool
val allHypsAndConcl : 'a Locus.clause_expr
val allHyps : 'a Locus.clause_expr
val onConcl : 'a Locus.clause_expr
val nowhere : 'a Locus.clause_expr
val onHyp : 'a -> 'a Locus.clause_expr
val is_nowhere : 'a Locus.clause_expr -> bool
val simple_clause_of : (unit -> Names.Id.t list) -> Locus.clause -> Locus.simple_clause
val concrete_clause_of : (unit -> Names.Id.t list) -> Locus.clause -> Locus.concrete_clause
val occurrences_of_goal : Locus.clause -> Locus.occurrences
val in_every_hyp : Locus.clause -> bool
val clause_with_generic_occurrences : 'a Locus.clause_expr -> bool
val clause_with_generic_context_selection : 'a Locus.clause_expr -> bool