The fresh_name generator has been moved to ProofEngineHelpers.

[helm.git] / helm / gTopLevel / primitiveTactics.mli

diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli
index 1fa97805ac50356a407448f5ca206c0a55fecd2b..59a714c78c938e3144f963a12390b54d332451f0 100644 (file)
--- a/helm/gTopLevel/primitiveTactics.mli
+++ b/helm/gTopLevel/primitiveTactics.mli
@@ -28,7 +28,7 @@ val apply_tac:
 val exact_tac:
   term: Cic.term -> ProofEngineTypes.tactic
 val intros_tac:
-  mknames: (unit -> string) -> ProofEngineTypes.tactic
+  ProofEngineTypes.tactic
 val cut_tac:
   term: Cic.term -> ProofEngineTypes.tactic 
 val letin_tac: