Module `Firstorder_plugin.Formula`Source

Sourceval qflag : bool Stdlib.ref

Sourceval red_flags : CClosure.RedFlags.reds Stdlib.ref

val (=?) : 
  ('a -> 'a -> int) ->
  ('b -> 'b -> int) ->
  'a ->
  'a ->
  'b ->
  'b ->
  int

val (==?) : 
  ('a -> 'a -> 'b -> 'b -> int) ->
  ('c -> 'c -> int) ->
  'a ->
  'a ->
  'b ->
  'b ->
  'c ->
  'c ->
  int

Sourcetype ('a, 'b) sum =

Sourcetype counter = bool -> Constr.metavariable

Sourceval construct_nhyps : Environ.env -> Constr.pinductive -> int array

val ind_hyps : 
  Environ.env ->
  Evd.evar_map ->
  int ->
  Constr.pinductive ->
  EConstr.constr list ->
  EConstr.rel_context array

Sourcetype atoms = {

}

Sourcetype side =

Sourceval dummy_id : Names.GlobRef.t

val build_atoms : 
  Environ.env ->
  Evd.evar_map ->
  counter ->
  side ->
  EConstr.constr ->
  bool * atoms

Sourcetype right_pattern =

Sourcetype left_arrow_pattern =

Sourcetype left_pattern =

Sourcetype t = {

}

val build_formula : 
  Environ.env ->
  Evd.evar_map ->
  side ->
  Names.GlobRef.t ->
  EConstr.types ->
  counter ->
  (t, EConstr.types) sum

Install