exception NotConvertible

  (* proof engine status *)
val proof : ProofEngineTypes.proof ref
val goal : ProofEngineTypes.goal ref

  (* start a new goal undoing part of the proof *)
val perforate : Cic.context -> Cic.term -> Cic.term -> unit

  (* reduction tactics *)
val whd : Cic.term -> unit
val reduce : Cic.term -> unit
val simpl : Cic.term -> unit
val fold : Cic.term -> unit
val change : goal_input:Cic.term -> input:Cic.term -> unit

  (* scratch area reduction tactics *)
val whd_in_scratch : Cic.term -> Cic.term -> Cic.term
val reduce_in_scratch : Cic.term -> Cic.term -> Cic.term
val simpl_in_scratch : Cic.term -> Cic.term -> Cic.term

  (* "primitive" tactics *)
val apply : Cic.term -> unit
val intros : unit -> unit
val cut : Cic.term -> unit
val letin : Cic.term -> unit
val exact : Cic.term -> unit
val elim_intros_simpl : Cic.term -> unit

  (* structural tactics *)
val clearbody : Cic.hypothesis -> unit
val clear : Cic.hypothesis -> unit

  (* other tactics *)
val elim_type : Cic.term -> unit
val ring : unit -> unit