X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=dfaf5b42426816f6f3dcfed8c333dc4c5565726a;hb=44b1f0c3a1e4bdc0abc3b02004c7b385ab63f7c5;hp=308144c21a6826e6a5d2952cdb24e977825a5e3e;hpb=d9b8131affff81514d792aa06d147b5375963b1f;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 308144c21..dfaf5b424 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -103,7 +103,6 @@ let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
       let t = disambiguate_lazy_term text prefix_len lexicon_status_ref t in
       `Unfold (Some t)
   | `Normalize
-  | `Reduce
   | `Simpl
   | `Unfold None
   | `Whd as kind -> kind