New argument (the hypothesis name) for cut.

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 5b5a76a7d0e6344fe0c1cdad993c9ce78b5bd696..650dbc9aab49b08b2583ccb30302026113803aaa 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -29,7 +29,9 @@ let tactic_of_ast = function
   | TacticAst.Contradiction _ -> Tactics.contradiction
   | TacticAst.Compare (_, term) -> Tactics.compare term
   | TacticAst.Constructor (_, n) -> Tactics.constructor n
-  | TacticAst.Cut (_, term) -> Tactics.cut term
+  | TacticAst.Cut (_, ident, term) ->
+     let names = match ident with None -> [] | Some id -> [id] in
+     Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
   | TacticAst.DecideEquality _ -> Tactics.decide_equality
   | TacticAst.Decompose (_,term) -> Tactics.decompose term
   | TacticAst.Discriminate (_,term) -> Tactics.discriminate term
@@ -394,9 +396,9 @@ let disambiguate_tactic status = function
       status, TacticAst.Constructor (loc,n)
   | TacticAst.Contradiction loc ->
       status, TacticAst.Contradiction loc
-  | TacticAst.Cut (loc, term) -> 
+  | TacticAst.Cut (loc, ident, term) -> 
       let status, cic = disambiguate_term status term in
-      status, TacticAst.Cut (loc, cic)
+      status, TacticAst.Cut (loc, ident, cic)
   | TacticAst.DecideEquality loc ->
       status, TacticAst.DecideEquality loc
   | TacticAst.Decompose (loc,term) ->