From 37b52567b8aa1bf5807767d94b96594c0e640588 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Mar 2010 10:21:14 +0000 Subject: [PATCH] nremark => `Example (not to be indexed) --- helm/software/components/ng_disambiguation/nCicDisambiguate.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2