The fresh_name generator has been moved to ProofEngineHelpers.

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

diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml
index eba2d571ff8d4fc26ed633f375f3be1fd89872cd..9a037d754d8acc3c37adbc830c41f90c382143fa 100644 (file)
--- a/helm/gTopLevel/primitiveTactics.ml
+++ b/helm/gTopLevel/primitiveTactics.ml
@@ -43,11 +43,7 @@ let lambda_abstract context newmeta ty mknames =
    function
       C.Cast (te,_)   -> collect_context context te
     | C.Prod (n,s,t)  ->
-       let n' =
-        match n with
-           C.Name _ -> n
-         | C.Anonymous -> C.Name (mknames ())
-       in
+       let n' = C.Name (mknames n) in
         let (context',ty,bo) =
          collect_context ((Some (n',(C.Decl s)))::context) t
         in
@@ -305,13 +301,15 @@ let apply_tac ~term ~status =
   with CicUnification.UnificationFailed as e ->
     raise (Fail (Printexc.to_string e))
 
-let intros_tac ~mknames ~status:(proof, goal) =
+let intros_tac ~status:(proof, goal) =
  let module C = Cic in
  let module R = CicReduction in
   let (_,metasenv,_,_) = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
    let newmeta = new_meta ~proof in
-    let (context',ty',bo') = lambda_abstract context newmeta ty mknames in
+    let (context',ty',bo') =
+     lambda_abstract context newmeta ty (ProofEngineHelpers.fresh_name)
+    in
      let (newproof, _) =
        subst_meta_in_proof proof metano bo' [newmeta,context',ty']
      in
@@ -507,7 +505,7 @@ let elim_simpl_intros_tac ~term =
   ~continuation:
    (Tacticals.then_
      ~start:(ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
-     ~continuation:(intros_tac ~mknames:(function () -> "FOO")))
+     ~continuation:intros_tac)
 ;;