Typing of intros_tac improved. It now has a parameter that is a fresh-names

[helm.git] / helm / gTopLevel / proofEngine.ml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index dbf04c393386c0d57e5e74faf57ec4e9b242092f..173c1c59d3195f374fe087513c8d188d411d9855 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -138,11 +138,10 @@ let perforate context term ty =
 
 (*CSC: generatore di nomi? Chiedere il nome? *)
 let fresh_name =
- let next_fresh_index = ref 0
-in
- function () ->
-  incr next_fresh_index ;
-  "fresh_name" ^ string_of_int !next_fresh_index
+ let next_fresh_index = ref 0 in
+  function () ->
+   incr next_fresh_index ;
+   "fresh_name" ^ string_of_int !next_fresh_index
 
 (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
 let reduction_tactic_in_scratch reduction_function term ty =
@@ -174,7 +173,7 @@ let simpl_in_scratch  = reduction_tactic_in_scratch ProofEngineReduction.simpl
 let can_apply term = can_apply_tactic (PrimitiveTactics.apply_tac ~term)
 let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
 let intros () =
-  apply_tactic (PrimitiveTactics.intros_tac ~name:(fresh_name ()))
+  apply_tactic (PrimitiveTactics.intros_tac ~mknames:fresh_name)
 let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term)
 let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term)
 let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)