X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=26c74e657afe317600598f3fe4e84f8886cf155d;hb=1589ec067f5f18594dfcab61431adbe095db1bd1;hp=f5ea66f2f6883e06a840744579277817577fe32f;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index f5ea66f2f..26c74e657 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -112,9 +112,6 @@ let disambiguate_tactic lexicon_status_ref context metasenv tactic =
         metasenv,GrafiteAst.Clear (loc,id)
     | GrafiteAst.ClearBody (loc,id) ->
        metasenv,GrafiteAst.ClearBody (loc,id)
-    | GrafiteAst.Compare (loc,term) ->
-        let metasenv,term = disambiguate_term context metasenv term in
-        metasenv,GrafiteAst.Compare (loc,term)
     | GrafiteAst.Constructor (loc,n) ->
         metasenv,GrafiteAst.Constructor (loc,n)
     | GrafiteAst.Contradiction loc ->
@@ -122,8 +119,6 @@ let disambiguate_tactic lexicon_status_ref context metasenv tactic =
     | GrafiteAst.Cut (loc, ident, term) -> 
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Cut (loc, ident, cic)
-    | GrafiteAst.DecideEquality loc ->
-        metasenv,GrafiteAst.DecideEquality loc
     | GrafiteAst.Decompose (loc, types, what, names) ->
         let disambiguate (metasenv,types) = function
            | GrafiteAst.Type _   -> assert false