(* The default of term is the thesis of the goal to be prooved *)
val unfold_tac:
- ProofEngineTypes.lazy_term option ->
+ Cic.lazy_term option ->
pattern:ProofEngineTypes.lazy_pattern ->
ProofEngineTypes.tactic
val change_tac:
pattern:ProofEngineTypes.lazy_pattern ->
- ProofEngineTypes.lazy_term ->
+ Cic.lazy_term ->
ProofEngineTypes.tactic
val fold_tac:
reduction:ProofEngineTypes.lazy_reduction ->
- term:ProofEngineTypes.lazy_term ->
+ term:Cic.lazy_term ->
pattern:ProofEngineTypes.lazy_pattern ->
ProofEngineTypes.tactic