package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t =
  1. | Regular
  2. | End_obligation of DeclareObl.obligation_qed_info
  3. | End_derive of {
    1. f : Names.Id.t;
    2. name : Names.Id.t;
    }
  4. | End_equations of {
    1. hook : Names.Constant.t list -> Evd.evar_map -> unit;
    2. i : Names.Id.t;
    3. types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list;
    4. wits : EConstr.t list ref;
    5. sigma : Evd.evar_map;
    }
OCaml

Innovation. Community. Security.