]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/tactics/reductionTactics.mli
made executable again
[helm.git] / helm / software / components / tactics / reductionTactics.mli
index f04e7dcac646ca9f14c961a62dcdbc183e85356b..004a3b3ee9f9a9faff5df8d018e2101a0405269b 100644 (file)
@@ -24,7 +24,6 @@
  *)
 
 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
 val head_beta_reduce_tac: ?delta:bool -> ?upto:int -> pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic