From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 18 Mar 2010 10:21:14 +0000 (+0000)
Subject: nremark => `Example (not to be indexed)
X-Git-Tag: make_still_working~2997
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=37b52567b8aa1bf5807767d94b96594c0e640588;p=helm.git

nremark => `Example (not to be indexed)
---

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