elim tactic: it needs two arguments, a term as well as a pattern

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

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