matitaGui: some missing cases during disambiguation now treated

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

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index e7f5eb1fd4077190f7d6d3f4b58be49699e9cd2b..7d110e2df6a5e4844d894d4ab96f2afb5ee92691 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -232,8 +232,6 @@ let disambiguate_tactic
         metasenv,GrafiteAst.Reduce(loc, red_kind, pattern)
     | GrafiteAst.Reflexivity loc ->
         metasenv,GrafiteAst.Reflexivity loc
-    | GrafiteAst.Rename (loc, froms, tos) ->
-        metasenv,GrafiteAst.Rename (loc, froms, tos)
     | GrafiteAst.Replace (loc, pattern, with_what) -> 
         let pattern = disambiguate_pattern pattern in
         let with_what = disambiguate_lazy_term with_what in