helm/gTopLevel/proofEngine.mli

   1
   2 exception NotConvertible
   3
   4   (* proof engine status *)
   5 val proof : ProofEngineTypes.proof ref
   6 val goal : ProofEngineTypes.goal ref
   7
   8   (* start a new goal undoing part of the proof *)
   9 val perforate : Cic.context -> Cic.term -> Cic.term -> unit
  10
  11   (* reduction tactics *)
  12 val whd : Cic.term -> unit
  13 val reduce : Cic.term -> unit
  14 val simpl : Cic.term -> unit
  15 val fold : Cic.term -> unit
  16 val change : goal_input:Cic.term -> input:Cic.term -> unit
  17
  18   (* scratch area reduction tactics *)
  19 val whd_in_scratch : Cic.term -> Cic.term -> Cic.term
  20 val reduce_in_scratch : Cic.term -> Cic.term -> Cic.term
  21 val simpl_in_scratch : Cic.term -> Cic.term -> Cic.term
  22
  23   (* "primitive" tactics *)
  24 val apply : Cic.term -> unit
  25 val intros : unit -> unit
  26 val cut : Cic.term -> unit
  27 val letin : Cic.term -> unit
  28 val exact : Cic.term -> unit
  29 val elim_intros_simpl : Cic.term -> unit
  30
  31   (* structural tactics *)
  32 val clearbody : Cic.hypothesis -> unit
  33 val clear : Cic.hypothesis -> unit
  34
  35   (* other tactics *)
  36 val elim_type : Cic.term -> unit
  37 val ring : unit -> unit
  38