]> matita.cs.unibo.it Git - helm.git/commitdiff
nremark => `Example (not to be indexed)
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 18 Mar 2010 10:21:14 +0000 (10:21 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 18 Mar 2010 10:21:14 +0000 (10:21 +0000)
helm/software/components/ng_disambiguation/nCicDisambiguate.ml

index 7ebca20d763f41043577fd1ed953f38fd987c10e..487bceb871377cfb1964e94ad81cccf878e8d733 100644 (file)
@@ -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