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 2d06942e309d0bc60901469ce4a9b5355ec5831c..7d110e2df6a5e4844d894d4ab96f2afb5ee92691 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -236,10 +236,10 @@ let disambiguate_tactic
         let pattern = disambiguate_pattern pattern in
         let with_what = disambiguate_lazy_term with_what in
         metasenv,GrafiteAst.Replace (loc, pattern, with_what)
-    | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
+    | GrafiteAst.Rewrite (loc, dir, t, pattern, names) ->
         let metasenv,term = disambiguate_term context metasenv t in
         let pattern = disambiguate_pattern pattern in
-        metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern)
+        metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern, names)
     | GrafiteAst.Right loc ->
         metasenv,GrafiteAst.Right loc
     | GrafiteAst.Ring loc ->