X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=487bceb871377cfb1964e94ad81cccf878e8d733;hb=8a218c35f9bde765a73f14867a294c874f9dc15c;hp=7ebca20d763f41043577fd1ed953f38fd987c10e;hpb=e9c6de34f4a1e784050a78db81787502cd112976;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 7ebca20d7..487bceb87 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -419,7 +419,7 @@ let new_flavour_of_flavour = function
   | `MutualDefinition -> `Definition 
   | `Fact -> `Fact
   | `Lemma -> `Lemma
-  | `Remark -> `Corollary
+  | `Remark -> `Example
   | `Theorem -> `Theorem
   | `Variant -> `Corollary 
   | `Axiom -> `Fact