X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;fp=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;h=e4f454ed61fd4cd3a0e80486470c01669b114544;hb=18b2b2742fe8ebb3d11b32b9bb727f510df6927a;hp=31e2093530f33d6a1c22dd601204c3cafa2b27e3;hpb=1e3ecdc411ef77f18c1d090b615f2dc665af0313;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 31e209353..e4f454ed6 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -71,13 +71,7 @@ type ('term, 'ident) tactic =
   | 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 *)