X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;h=e4f454ed61fd4cd3a0e80486470c01669b114544;hb=08791e80816548121e81e04d3ead8c9a5171d033;hp=31e2093530f33d6a1c22dd601204c3cafa2b27e3;hpb=fddf15f1e9d253316bdcb854c2ff7ec64144bde8;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 *)