* http://cs.unibo.it/helm/.
*)
-val simpl_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
-val reduce_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
-val whd_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
-val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
+val simpl_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+val reduce_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+val whd_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+val normalize_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
(* The default of term is the thesis of the goal to be prooved *)
val unfold_tac:
- ProofEngineTypes.lazy_term option ->
- pattern:ProofEngineTypes.pattern ->
+ Cic.lazy_term option ->
+ pattern:ProofEngineTypes.lazy_pattern ->
ProofEngineTypes.tactic
val change_tac:
- pattern:ProofEngineTypes.pattern ->
- ProofEngineTypes.lazy_term ->
+ pattern:ProofEngineTypes.lazy_pattern ->
+ Cic.lazy_term ->
ProofEngineTypes.tactic
val fold_tac:
reduction:ProofEngineTypes.lazy_reduction ->
- term:ProofEngineTypes.lazy_term ->
- pattern:ProofEngineTypes.pattern ->
+ term:Cic.lazy_term ->
+ pattern:ProofEngineTypes.lazy_pattern ->
ProofEngineTypes.tactic