package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'a or_var =
  1. | ArgArg of 'a
  2. | ArgVar of Names.lident
type !'a occurrences_gen =
  1. | AllOccurrences
  2. | AtLeastOneOccurrence
  3. | AllOccurrencesBut of 'a list
  4. | NoOccurrences
  5. | OnlyOccurrences of 'a list
type occurrences_expr = int or_var occurrences_gen
type !'a with_occurrences = occurrences_expr * 'a
type occurrences = int occurrences_gen
type hyp_location_flag =
  1. | InHyp
  2. | InHypTypeOnly
  3. | InHypValueOnly
type !'a hyp_location_expr = 'a with_occurrences * hyp_location_flag
type !'id clause_expr = {
  1. onhyps : 'id hyp_location_expr list option;
  2. concl_occs : occurrences_expr;
}
type clause = Names.Id.t clause_expr
type clause_atom =
  1. | OnHyp of Names.Id.t * occurrences_expr * hyp_location_flag
  2. | OnConcl of occurrences_expr
type concrete_clause = clause_atom list
type hyp_location = Names.Id.t * hyp_location_flag
type goal_location = hyp_location option
type simple_clause = Names.Id.t option list
type !'a or_like_first =
  1. | AtOccs of 'a
  2. | LikeFirst