From 96c2feeb6b1d27e25b7bca582ff6c25a4f87dca8 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 5 Nov 2004 11:03:43 +0000 Subject: [PATCH] ported to new cut and letin "API" --- helm/gTopLevel/proofEngine.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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) -- 2.39.2