| Symmetry of loc
| Transitivity of loc * 'term
-type thm_flavour =
- [ `Definition
- | `Fact
- | `Lemma
- | `Remark
- | `Theorem
- ]
+type thm_flavour = Cic.object_flavour
(** <name, inductive/coinductive, type, constructor list>
* true means inductive, false coinductive *)