Never implemented tactics compare and decide equality purged from the code.

[helm.git] / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index f5ea66f2f6883e06a840744579277817577fe32f..26c74e657afe317600598f3fe4e84f8886cf155d 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/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