From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 5 Nov 2004 11:03:43 +0000 (+0000)
Subject: ported to new cut and letin "API"
X-Git-Tag: v_0_6_4_1~24
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=96c2feeb6b1d27e25b7bca582ff6c25a4f87dca8;p=helm.git

ported to new cut and letin "API"
---

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index ac1119dd5..9292ece0b 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -183,9 +183,9 @@ let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
 let intros ?mk_fresh_name_callback () =
  apply_tactic (PrimitiveTactics.intros_tac ?mk_fresh_name_callback ())
 let cut ?mk_fresh_name_callback term =
- apply_tactic (PrimitiveTactics.cut_tac ?mk_fresh_name_callback term)
+ apply_tactic (PrimitiveTactics.cut_tac ?mk_fresh_name_callback ~term)
 let letin ?mk_fresh_name_callback term =
- apply_tactic (PrimitiveTactics.letin_tac ?mk_fresh_name_callback term)
+ apply_tactic (PrimitiveTactics.letin_tac ?mk_fresh_name_callback ~term)
 let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
 let elim_intros_simpl term =
   apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term)