name specifications added for elim_intros, elim_intros_simpl and elim_type

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 0e46c34d2236549a834ee624b2f11c353f4f1ea8..7f70736abbe22a30cbae66fcaf8db893429e49c2 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -40,9 +40,10 @@ let tactic_of_ast = function
   | TacticAst.DecideEquality _ -> Tactics.decide_equality
   | TacticAst.Decompose (_,term) -> Tactics.decompose term
   | TacticAst.Discriminate (_,term) -> Tactics.discriminate term
-  | TacticAst.Elim (_, term, _) ->
-      Tactics.elim_intros term
-  | TacticAst.ElimType (_, term) -> Tactics.elim_type term
+  | TacticAst.Elim (_, what, using, depth, names) ->
+      Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
+  | TacticAst.ElimType (_, what, using, depth, names) ->
+      Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
   | TacticAst.Exact (_, term) -> Tactics.exact term
   | TacticAst.Exists _ -> Tactics.exists
   | TacticAst.Fail _ -> Tactics.fail
@@ -447,16 +448,20 @@ let disambiguate_tactic status = function
   | TacticAst.Exact (loc, term) -> 
       let status, cic = disambiguate_term status term in
       status, TacticAst.Exact (loc, cic)
-  | TacticAst.Elim (loc, term, Some term') ->
-      let status, cic1 = disambiguate_term status term in
-      let status, cic2 = disambiguate_term status term' in
-      status, TacticAst.Elim (loc, cic1, Some cic2)
-  | TacticAst.Elim (loc, term, None) ->
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.Elim (loc, cic, None)
-  | TacticAst.ElimType (loc, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.ElimType (loc, cic)
+  | TacticAst.Elim (loc, what, Some using, depth, idents) ->
+      let status, what = disambiguate_term status what in
+      let status, using = disambiguate_term status using in
+      status, TacticAst.Elim (loc, what, Some using, depth, idents)
+  | TacticAst.Elim (loc, what, None, depth, idents) ->
+      let status, what = disambiguate_term status what in
+      status, TacticAst.Elim (loc, what, None, depth, idents)
+  | TacticAst.ElimType (loc, what, Some using, depth, idents) ->
+      let status, what = disambiguate_term status what in
+      let status, using = disambiguate_term status using in
+      status, TacticAst.ElimType (loc, what, Some using, depth, idents)
+  | TacticAst.ElimType (loc, what, None, depth, idents) ->
+      let status, what = disambiguate_term status what in
+      status, TacticAst.ElimType (loc, what, None, depth, idents)
   | TacticAst.Exists loc -> status, TacticAst.Exists loc 
   | TacticAst.Fail loc -> status,TacticAst.Fail loc
   | TacticAst.Fold (loc,reduction_kind, term, pattern) ->