]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/ring.mli
we were generating a name for the main fix twice
[helm.git] / helm / software / components / tactics / ring.mli
1
2   (* ring tactics *)
3 val ring_tac: ProofEngineTypes.tactic
4
5 (*Galla: spostata in variuosTactics.ml
6   (* auxiliary tactics *)
7 val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic
8 *)
9
10 (* spostata in variousTactics.ml
11 val reflexivity_tac: ProofEngineTypes.tactic
12 *)