package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type mutable_flag = bool
type rec_flag = bool
type redef_flag = bool
type lid = Names.Id.t
type uid = Names.Id.t
type ltac_constant = Names.KerName.t
type ltac_alias = Names.KerName.t
type ltac_constructor = Names.KerName.t
type ltac_projection = Names.KerName.t
type type_constant = Names.KerName.t
type tacref =
  1. | TacConstant of ltac_constant
  2. | TacAlias of ltac_alias
type 'a or_relid =
  1. | RelId of Libnames.qualid
  2. | AbsKn of 'a
Misc
type ml_tactic_name = {
  1. mltac_plugin : string;
  2. mltac_tactic : string;
}
type 'a or_tuple =
  1. | Tuple of int
  2. | Other of 'a
Type syntax
type raw_typexpr_r =
  1. | CTypVar of Names.Name.t
  2. | CTypArrow of raw_typexpr * raw_typexpr
  3. | CTypRef of type_constant or_tuple or_relid * raw_typexpr list
and raw_typexpr = raw_typexpr_r CAst.t
type raw_typedef =
  1. | CTydDef of raw_typexpr option
  2. | CTydAlg of (uid * raw_typexpr list) list
  3. | CTydRec of (lid * mutable_flag * raw_typexpr) list
  4. | CTydOpn
type 'a glb_typexpr =
  1. | GTypVar of 'a
  2. | GTypArrow of 'a glb_typexpr * 'a glb_typexpr
  3. | GTypRef of type_constant or_tuple * 'a glb_typexpr list
type glb_alg_type = {
  1. galg_constructors : (uid * int glb_typexpr list) list;
    (*

    Constructors of the algebraic type

    *)
  2. galg_nconst : int;
    (*

    Number of constant constructors

    *)
  3. galg_nnonconst : int;
    (*

    Number of non-constant constructors

    *)
}
type glb_typedef =
  1. | GTydDef of int glb_typexpr option
  2. | GTydAlg of glb_alg_type
  3. | GTydRec of (lid * mutable_flag * int glb_typexpr) list
  4. | GTydOpn
type type_scheme = int * int glb_typexpr
type raw_quant_typedef = Names.lident list * raw_typedef
type glb_quant_typedef = int * glb_typedef
Term syntax
type atom =
  1. | AtmInt of int
  2. | AtmStr of string
type raw_patexpr_r =
  1. | CPatVar of Names.Name.t
  2. | CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
  3. | CPatCnv of raw_patexpr * raw_typexpr

Tactic expressions

and raw_patexpr = raw_patexpr_r CAst.t
type raw_tacexpr_r =
  1. | CTacAtm of atom
  2. | CTacRef of tacref or_relid
  3. | CTacCst of ltac_constructor or_tuple or_relid
  4. | CTacFun of raw_patexpr list * raw_tacexpr
  5. | CTacApp of raw_tacexpr * raw_tacexpr list
  6. | CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr
  7. | CTacCnv of raw_tacexpr * raw_typexpr
  8. | CTacSeq of raw_tacexpr * raw_tacexpr
  9. | CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr
  10. | CTacCse of raw_tacexpr * raw_taccase list
  11. | CTacRec of raw_recexpr
  12. | CTacPrj of raw_tacexpr * ltac_projection or_relid
  13. | CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr
  14. | CTacExt : ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr_r
and raw_tacexpr = raw_tacexpr_r CAst.t
and raw_taccase = raw_patexpr * raw_tacexpr
and raw_recexpr = (ltac_projection or_relid * raw_tacexpr) list
type case_info = type_constant or_tuple
type 'a open_match = {
  1. opn_match : 'a;
  2. opn_branch : (Names.Name.t * Names.Name.t array * 'a) Names.KNmap.t;
    (*

    Invariant: should not be empty

    *)
  3. opn_default : Names.Name.t * 'a;
}
type glb_tacexpr =
  1. | GTacAtm of atom
  2. | GTacVar of Names.Id.t
  3. | GTacRef of ltac_constant
  4. | GTacFun of Names.Name.t list * glb_tacexpr
  5. | GTacApp of glb_tacexpr * glb_tacexpr list
  6. | GTacLet of rec_flag * (Names.Name.t * glb_tacexpr) list * glb_tacexpr
  7. | GTacCst of case_info * int * glb_tacexpr list
  8. | GTacCse of glb_tacexpr * case_info * glb_tacexpr array * (Names.Name.t array * glb_tacexpr) array
  9. | GTacPrj of type_constant * glb_tacexpr * int
  10. | GTacSet of type_constant * glb_tacexpr * int * glb_tacexpr
  11. | GTacOpn of ltac_constructor * glb_tacexpr list
  12. | GTacWth of glb_tacexpr open_match
  13. | GTacExt : (_, 'a) Tac2dyn.Arg.tag * 'a -> glb_tacexpr
  14. | GTacPrm of ml_tactic_name * glb_tacexpr list
Parsing & Printing
type exp_level =
  1. | E5
  2. | E4
  3. | E3
  4. | E2
  5. | E1
  6. | E0
type sexpr =
  1. | SexprStr of string CAst.t
  2. | SexprInt of int CAst.t
  3. | SexprRec of Loc.t * Names.Id.t option CAst.t * sexpr list
Toplevel statements
type strexpr =
  1. | StrVal of mutable_flag * rec_flag * (Names.lname * raw_tacexpr) list
    (*

    Term definition

    *)
  2. | StrTyp of rec_flag * (Libnames.qualid * redef_flag * raw_quant_typedef) list
    (*

    Type definition

    *)
  3. | StrPrm of Names.lident * raw_typexpr * ml_tactic_name
    (*

    External definition

    *)
  4. | StrSyn of sexpr list * int option * raw_tacexpr
    (*

    Syntactic extensions

    *)
  5. | StrMut of Libnames.qualid * Names.lident option * raw_tacexpr
    (*

    Redefinition of mutable globals

    *)
Dynamic semantics

Values are represented in a way similar to OCaml, i.e. they contrast immediate integers (integers, constructors without arguments) and structured blocks (tuples, arrays, constructors with arguments), as well as a few other base cases, namely closures, strings, named constructors, and dynamic type coming from the Coq implementation.

type tag = int
type frame =
  1. | FrLtac of ltac_constant
  2. | FrAnon of glb_tacexpr
  3. | FrPrim of ml_tactic_name
  4. | FrExtn : ('a, 'b) Tac2dyn.Arg.tag * 'b -> frame
type backtrace = frame list