PrimitiveTactics: intros _ now aveilable

[helm.git] / components / tactics / primitiveTactics.ml

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 64db996667879cd10efb1adf0ad83b7032fd2a94..c5aab0f5ff45eeebb63f608195552302d799df26 100644 (file)
--- a/components/tactics/primitiveTactics.ml
+++ b/components/tactics/primitiveTactics.ml
@@ -52,9 +52,13 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name =
       match ty with 
         C.Cast (te,_)   -> collect_context context howmany do_whd te 
       | C.Prod (n,s,t)  ->
-         let n' = mk_fresh_name metasenv context n ~typ:s in
+        let n' = mk_fresh_name metasenv context n ~typ:s in
           let (context',ty,bo) =
-           let ctx = (Some (n',(C.Decl s)))::context in
+           let entry = match n' with
+             | C.Name _    -> Some (n',(C.Decl s))
+             | C.Anonymous -> None
+          in
+          let ctx = entry :: context in
            collect_context ctx (howmany - 1) do_whd t 
           in
            (context',ty,C.Lambda(n',s,bo))
@@ -365,9 +369,7 @@ let apply_tac ~term =
   PET.mk_tactic (apply_tac ~term)
 
 let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ()=
- let intros_tac
-  ?(mk_fresh_name_callback = (FreshNamesGenerator.mk_fresh_name ~subst:[])) ()
-  (proof, goal)
+ let intros_tac (proof, goal)
  =
   let module C = Cic in
   let module R = CicReduction in
@@ -383,7 +385,7 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_
       in
        (newproof, [newmeta])
  in
-  PET.mk_tactic (intros_tac ~mk_fresh_name_callback ())
+  PET.mk_tactic intros_tac
   
 let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
  let cut_tac
@@ -706,7 +708,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
    PET.mk_tactic elim_tac
 ;;
 
-let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
+let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
  let cases_tac ~term (proof, goal) =
   let module TC = CicTypeChecker in
   let module U = UriManager in