PrimitiveTactics: intros _ now aveilable

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

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 912abbcc38d0eadb1dc1235d35010309e719d3e8..fd1849760f986010be8a950833a5bf8eb47aca11 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -212,22 +212,22 @@ let rec 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, pattern, depth, idents) ->
+    | GrafiteAst.Elim (loc, what, Some using, pattern, specs) ->
        let metasenv,what = disambiguate_term context metasenv what in
         let metasenv,using = disambiguate_term context metasenv using in
        let pattern = disambiguate_pattern pattern in
-        metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, depth, idents)
-    | GrafiteAst.Elim (loc, what, None, pattern, depth, idents) ->
+        metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, specs)
+    | GrafiteAst.Elim (loc, what, None, pattern, specs) ->
        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) ->
+        metasenv,GrafiteAst.Elim (loc, what, None, pattern, specs)
+    | GrafiteAst.ElimType (loc, what, Some using, specs) ->
         let metasenv,what = disambiguate_term context metasenv what in
         let metasenv,using = disambiguate_term context metasenv using in
-        metasenv,GrafiteAst.ElimType (loc, what, Some using, depth, idents)
-    | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
+        metasenv,GrafiteAst.ElimType (loc, what, Some using, specs)
+    | GrafiteAst.ElimType (loc, what, None, specs) ->
         let metasenv,what = disambiguate_term context metasenv what in
-        metasenv,GrafiteAst.ElimType (loc, what, None, depth, idents)
+        metasenv,GrafiteAst.ElimType (loc, what, None, specs)
     | GrafiteAst.Exists loc ->
         metasenv,GrafiteAst.Exists loc 
     | GrafiteAst.Fail loc ->
@@ -246,8 +246,8 @@ let rec disambiguate_tactic
         metasenv,GrafiteAst.Generalize (loc,pattern,ident)
     | GrafiteAst.IdTac loc ->
         metasenv,GrafiteAst.IdTac loc
-    | GrafiteAst.Intros (loc, num, names) ->
-        metasenv,GrafiteAst.Intros (loc, num, names)
+    | GrafiteAst.Intros (loc, specs) ->
+        metasenv,GrafiteAst.Intros (loc, specs)
     | GrafiteAst.Inversion (loc, term) ->
        let metasenv,term = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Inversion (loc, term)