elim tactic: now takes a pattern instead of just a term

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

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index cc8360c28f51d0728996cdb37c7851e11cd69965..97f0d5e85892df5b5933cf706d5b5e69d9ec2144 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -158,13 +158,13 @@ let disambiguate_tactic
     | GrafiteAst.Exact (loc, term) -> 
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Exact (loc, cic)
-    | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
-        let metasenv,what = disambiguate_term context metasenv what in
+    | GrafiteAst.Elim (loc, pattern, Some using, depth, idents) ->
+       let pattern = disambiguate_pattern pattern in
         let metasenv,using = disambiguate_term context metasenv using in
-        metasenv,GrafiteAst.Elim (loc, what, Some using, depth, idents)
-    | GrafiteAst.Elim (loc, what, None, depth, idents) ->
-        let metasenv,what = disambiguate_term context metasenv what in
-        metasenv,GrafiteAst.Elim (loc, what, None, depth, idents)
+        metasenv,GrafiteAst.Elim (loc, pattern, Some using, depth, idents)
+    | GrafiteAst.Elim (loc, pattern, None, depth, idents) ->
+       let pattern = disambiguate_pattern pattern in
+        metasenv,GrafiteAst.Elim (loc, pattern, None, depth, idents)
     | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
         let metasenv,what = disambiguate_term context metasenv what in
         let metasenv,using = disambiguate_term context metasenv using in